投影時序邏輯（Projection Temporal Logic, PTL）是一階區(qū)間時序邏輯（Interval Temporal Logic, ITL）的擴展,引入了全新的投影操作符prj,并且同時支持有窮和無窮模型,具備了完全正則表達式的表達能力,能夠方便的描述順序、選擇、循環(huán)、并行、信號量等程序結(jié)構(gòu),可在同一PTL邏輯框架內(nèi)完成對待驗證系統(tǒng)的建模和性質(zhì)描述,適用于各類軟硬件系統(tǒng)的驗證.為采用定理證明的方法對并發(fā)及交互式系統(tǒng)驗證,本文在有窮論域的前提下為PTL建立了一個完備公理系統(tǒng),提出了PTL的范式（Normal Form, NF）、范式圖（Normal Form Graph, NFG）、標記范式（Labeled Normal Form, LNF）和標記范式圖（Labeled Normal Form Graph, LNFG）技術(shù),利用NFG和LNFG可描述PTL公式模型的特性分別解決了有窮和無窮時間PTL的判定問題,并證明了有窮時間和無窮時間PTL公理系統(tǒng)的完備性,同時探討了PTL的表達能力和基于PTL的系統(tǒng)建模方法,為使用PTL進行形式化驗證打下了堅實的理論基礎(chǔ)。本文的主要貢獻... 

【文章來源】：西安電子科技大學(xué)陜西省 211工程院校 教育部直屬院校

【文章頁數(shù)】：161 頁

【學(xué)位級別】：博士

【文章目錄】：
摘要
Abstract
第一章 緒論
    1.1 研究背景與意義
    1.2 形式化方法
        1.2.1 模型檢測
        1.2.2 定理證明
    1.3 時序邏輯
    1.4 相關(guān)研究工作
    1.5 論文的主要工作與組織結(jié)構(gòu)
第二章 投影時序邏輯
    2.1 語法
    2.2 語義
    2.3 PTL操作符特點分析
    2.4 一些特殊形式的PTL公式
    2.5 小結(jié)
第三章 PTL的公理系統(tǒng)
    3.1 PTL的公理系統(tǒng)
    3.2 公理系統(tǒng)的可靠性
    3.3 常用定理
    3.4 小結(jié)
第四章 有窮時間PTL公理系統(tǒng)的完備性
    4.1 PTL的范式
        4.1.1 范式的定義
        4.1.2 范式的存在性
        4.1.3 范式的計算算法
    4.2 范式圖
        4.2.1 范式圖的定義
        4.2.2 范式圖的構(gòu)造算法
        4.2.3 范式圖的一些性質(zhì)
        4.2.4 范式圖的局限性
    4.3 有窮時間PTL的判定算法
    4.4 有窮時間公理系統(tǒng)的完備性證明
    4.5 小結(jié)
第五章 無窮時間PTL公理系統(tǒng)的完備性
    5.1 標記范式與標記范式圖的引入
    5.2 標記范式
        5.2.1 標記范式的定義
        5.2.2 標記范式的計算算法
    5.3 標記范式圖
    5.4 QFPTL公式的判定算法
        5.4.1 QFPTL公式LNFG的特殊性質(zhì)
        5.4.2 LNFG的化簡
        5.4.3 QFPTL的判定算法
        5.4.4 QFPTL的判定實例
    5.5 PTL公式的判定算法
        5.5.1 從QPTL到QFPTL的轉(zhuǎn)換
        5.5.2 PTL的判定算法
    5.6 PTL公理系統(tǒng)的完備性證明
    5.7 小結(jié)
第六章 基于PTL的形式化驗證
    6.1 PTL與完全正則語言
        6.1.1 完全正則語言
        6.1.2 從FRE到PTL公式
        6.1.3 從PTL公式到FRE
    6.2 使用PTL進行系統(tǒng)建模
        6.2.1 MSVL
        6.2.2 擴展Kripke結(jié)構(gòu)
    6.3 驗證實例
        6.3.1 問題描述
        6.3.2 系統(tǒng)建模
        6.3.3 系統(tǒng)驗證
    6.4 小結(jié)
第七章 總結(jié)與展望
    7.1 論文總結(jié)
    7.2 進一步的研究展望
致謝
參考文獻
攻讀博士學(xué)位期間的研究成果


【參考文獻】：
期刊論文
[1]面向命題投影時序邏輯的安全協(xié)議模型檢測[J]. 楊琛,段振華,王小兵.  西安交通大學(xué)學(xué)報. 2010(08)
[2]利用投影時序邏輯的多內(nèi)核進程調(diào)度建模與驗證[J]. 舒新峰,段振華.  西安交通大學(xué)學(xué)報. 2010(03)
[3]投影時序邏輯的公理系統(tǒng)與形式驗證[J]. 舒新峰,段振華.  西安電子科技大學(xué)學(xué)報. 2009(04)
[4]面向投影時序邏輯的Web服務(wù)模型檢測[J]. 王小兵,段振華.  西安交通大學(xué)學(xué)報. 2009(04)
[5]混合投影時序邏輯與混合系統(tǒng)的形式化驗證[J]. 張海賓,段振華.  計算機科學(xué). 2007(11)
[6]基于擴展投影時序邏輯的組合Web服務(wù)描述與驗證[J]. 雷麗暉,段振華.  西安交通大學(xué)學(xué)報. 2007(10)
[7]使用擴展區(qū)間時序邏輯為并發(fā)工作流建模[J]. 雷麗暉,段振華.  西安電子科技大學(xué)學(xué)報. 2007(04)



本文編號：3290350