行為、事件具有實(shí)時(shí)關(guān)系的軟件或硬件系統(tǒng)構(gòu)成了實(shí)時(shí)(計(jì)算)系統(tǒng)。在交通控制,航空航天等一系列對(duì)安全性要求極高的應(yīng)用領(lǐng)域,實(shí)時(shí)系統(tǒng)的形式化驗(yàn)證成為保證系統(tǒng)正確性的重要手段。實(shí)時(shí)模型檢測(cè)就是其中的一類自動(dòng)驗(yàn)證方法,原理是實(shí)時(shí)邏輯公式描述系統(tǒng)所需滿足的性質(zhì),時(shí)間自動(dòng)機(jī)建立系統(tǒng)模型,驗(yàn)證算法自動(dòng)判定模型是否滿足性質(zhì)。實(shí)時(shí)邏輯有很多種,用于形式化描述與驗(yàn)證也各有其優(yōu)勢(shì),時(shí)間區(qū)間時(shí)序邏輯就是其中的一種線性實(shí)時(shí)邏輯,并已被應(yīng)用于對(duì)一些實(shí)時(shí)系統(tǒng)的形式化描述與分析中。雖然該邏輯有其獨(dú)特的比較優(yōu)勢(shì),然而到目前為止,時(shí)間區(qū)間時(shí)序邏輯還不能用于實(shí)時(shí)系統(tǒng)的模型檢測(cè),因?yàn)槿鄙衮?yàn)證方法,也沒有支撐方法的形式化理論來加深人們對(duì)該邏輯的理解和認(rèn)識(shí)。針對(duì)于此,本文研究命題部分的時(shí)間區(qū)間時(shí)序邏輯模型檢測(cè)問題,以該問題為主線,從理論、方法、應(yīng)用三個(gè)層面構(gòu)建其體系。 為了搞清楚該邏輯可以描述哪些性質(zhì)、是否可應(yīng)用于模型檢測(cè)以及模型檢測(cè)的效率,本文分別從邏輯的表達(dá)能力、判定性及復(fù)雜性三個(gè)方面進(jìn)行研究,從而形成該邏輯模型檢測(cè)的形式化理論。證明了離散時(shí)間域上的該邏輯與離散時(shí)間正則表達(dá)式、離散時(shí)間自動(dòng)機(jī)等價(jià),結(jié)果表明一切離散時(shí)間正則語言均...

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

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

【文章目錄】：
摘要
ABSTRACT
第一章 緒論
    1.1 研究背景與研究現(xiàn)狀
        1.1.1 模型檢測(cè)
        1.1.2 區(qū)間時(shí)序邏輯
        1.1.3 實(shí)時(shí)系統(tǒng)模型檢測(cè)
        1.1.4 時(shí)段演算
        1.1.5 基于模型檢測(cè)的入侵檢測(cè)
    1.2 存在的問題及本文工作
    1.3 論文組織結(jié)構(gòu)
第二章 時(shí)序邏輯
    2.1 命題投影時(shí)序邏輯
        2.1.1、語法
        2.1.2、語義
        2.1.3、導(dǎo)出公式
    2.2 命題區(qū)間時(shí)序邏輯
        2.2.1、語法
        2.2.2 語義
        2.2.3 導(dǎo)出公式
    2.3 正則圖算法與滿足性判定
        2.3.1 正則形
        2.3.2 正則圖
    2.4 復(fù)雜度分析
    2.5 chop star 公式的滿足性判定
        2.5.1 擴(kuò)展命題區(qū)間時(shí)序邏輯EPITL
        2.5.2 EPITL 可滿足性判定
        2.5.3 EPITL 可滿足性判定問題固有復(fù)雜度與算法復(fù)雜度
    2.6 小結(jié)
第三章 實(shí)時(shí)邏輯與自動(dòng)機(jī)
    3.1 時(shí)間區(qū)間時(shí)序邏輯
dense-R">        3.1.1 實(shí)界稠密時(shí)間區(qū)間時(shí)序邏輯TITL_<sub>dense-R
dense-N">        3.1.2 整界稠密時(shí)間區(qū)間時(shí)序邏輯TITL_<sub>dense-N
        3.1.3 實(shí)樣本時(shí)間區(qū)間時(shí)序邏輯TITLsample-R

        3.1.4 整樣本時(shí)間區(qū)間時(shí)序邏輯TITL_sample-N

        3.1.5 TITL_<sub>dense-R 、TITL_<sub>dense-N 、TITL_sample-R 和TITL_sample-N 的關(guān)系
    3.2 時(shí)間自動(dòng)機(jī)
        3.2.1、稠密時(shí)間自動(dòng)機(jī)
        3.2.2、離散時(shí)間自動(dòng)機(jī)
    3.3 時(shí)間正則表達(dá)式
        3.3.1、有窮時(shí)間
        3.3.2、無窮時(shí)間
    3.4 離散時(shí)段演算
    3.5 小結(jié)
第四章 TITL 公式可滿足性判定
    4.1 TITL_N公式可滿足性的判定問題
        4.1.1 時(shí)間正則圖
        4.1.2 TITL_N公式可滿足性判定算法
        4.1.3 兩個(gè)例子
        4.1.4 復(fù)雜度分析
        4.1.5 相關(guān)工作比較
    4.2 TITL_R公式可滿足性的判定問題
        4.2.1 TITL_R公式可滿足性的不可判定性
        4.2.2 有關(guān)TITL_R公式判定性與復(fù)雜性結(jié)論
    4.3 小結(jié)
第五章 TITL 模型檢測(cè)
    5.1 離散TITL 模型檢測(cè)
    5.2 稠密TITL 模型檢測(cè)
    5.3 相關(guān)工作比較
        5.3.1 基于非時(shí)間化的TITL_N判定算法的抽象描述與分析
        5.3.2 兩種方法比較
    5.4 小結(jié)
第六章 離散TITL 表達(dá)能力
    6.1 TITL_N
*

        6.1.1 語法
        6.1.2 語義
    6.2 TITL_N
*→TAN

    6.3 TA_N→TRE_N

    6.4 TRE_N→TITL_N
*

    6.5 TITLN
*、TA_N、TRE_N的等價(jià)性定理
    6.6 TITL_N與{┌w┐,l=k}-DC_N}的等價(jià)定理
    6.7 小結(jié)
第七章 統(tǒng)一邏輯框架模型檢測(cè)
    7.1 命題投影時(shí)序邏輯統(tǒng)一模型檢測(cè)
        7.1.1 PPTL 順序模型
        7.1.2 PPTL 并發(fā)模型
        7.1.3 一個(gè)模型檢測(cè)實(shí)例
    7.2 離散時(shí)間區(qū)間時(shí)序邏輯統(tǒng)一模型檢測(cè)
        7.2.1、使用 TITLN建立系統(tǒng)模型
        7.2.2、一個(gè)實(shí)例
        7.2.3、TITLN統(tǒng)一框架模型檢測(cè)
    7.3 小結(jié)
第八章 基于時(shí)間區(qū)間時(shí)序邏輯的入侵檢測(cè)
    8.1 攻擊簽名邏輯與入侵檢測(cè)
        8.1.1 攻擊簽名邏輯
        8.1.2 攻擊模式的區(qū)間時(shí)序邏輯模型
        8.1.3 實(shí)例研究
        8.1.4 基于區(qū)間時(shí)序邏輯模型檢測(cè)的入侵檢測(cè)算法
        8.1.5 prj + prj star 與 chop + chop star 的表達(dá)能力
    8.2 實(shí)時(shí)攻擊簽名邏輯與入侵檢測(cè)
        8.2.1 實(shí)時(shí)攻擊簽名邏輯
        8.2.2 基于 RASL 模型檢測(cè)的入侵檢測(cè)
        8.2.3 實(shí)例研究
        8.2.4 相關(guān)工作比較
    8.3 小結(jié)
第九章 結(jié)論與展望
    9.1 本文結(jié)論與創(chuàng)新點(diǎn)
    9.2 下一步研究方向
致謝
參考文獻(xiàn)
攻讀博士學(xué)位期間完成的研究論文



本文編號(hào)：3739387

boshi