基于BDDs的離散實(shí)時(shí)時(shí)態(tài)邏輯RTCTL-的符號(hào)化模型檢測(cè)及證據(jù)生成.pdf

1、模型檢測(cè)是公認(rèn)的一種比較有效的驗(yàn)證系統(tǒng)正確性和可靠性的方法。在一些安全至關(guān)重要的領(lǐng)域檢測(cè)預(yù)知系統(tǒng)的響應(yīng)時(shí)間、事件調(diào)度的延遲等一系列的參數(shù)尤為重要。實(shí)際上大部分的實(shí)時(shí)系統(tǒng)都有自己的有效活動(dòng)時(shí)間，即我們只需要檢測(cè)其在某段時(shí)間內(nèi)的性能和參數(shù)，也就是對(duì)離散實(shí)時(shí)系統(tǒng)的模型檢測(cè)。因此對(duì)離散實(shí)時(shí)時(shí)態(tài)邏輯的模型檢測(cè)便成為課題組要解決的關(guān)鍵問(wèn)題，Real-Time Temporal Logic RTCTL*從很大程度上擴(kuò)展了邏輯描述范圍，是一種表達(dá)力更強(qiáng)

2、的規(guī)范描述邏輯，因此對(duì) RTCTL*的研究在形式化驗(yàn)證領(lǐng)域中有著重要的影響和意義。
　　論文的主要研究工作概括如下：
　　1．根據(jù)離散實(shí)時(shí)系統(tǒng)的特征與性質(zhì)提出并構(gòu)造了弱公平性約束的有限狀態(tài)遷移系統(tǒng) Just Discrete System（JDS)作為計(jì)算模型，并對(duì)JDS之間的同步并行計(jì)算規(guī)則進(jìn)行了詳細(xì)的定義；
　　2．在 CTL*語(yǔ)法和語(yǔ)義的基礎(chǔ)上擴(kuò)展定義并解釋了 RTCTL*的語(yǔ)法和語(yǔ)義，并通過(guò)一系列的等式轉(zhuǎn)換添加

3、了一些額外的操作到 RTCTL*中；
　　3．通過(guò)將 RTCTL*公式映射為狀態(tài)公式，把 RTCTL*的符號(hào)化模型檢測(cè)問(wèn)題轉(zhuǎn)化為 CTL的模型檢測(cè)問(wèn)題，并對(duì)不同類(lèi)型的RTCTL*公式在模型檢測(cè)過(guò)程中需要借助的第三者（temporal tester）給出構(gòu)造方法，提出了基于 BDDs的離散實(shí)時(shí)時(shí)態(tài)邏輯 RTCTL*的符號(hào)化模型檢測(cè)算法，并從理論上證明了算法的可靠性和完備性；
　　4．論證了生成反例與產(chǎn)生證據(jù)這兩個(gè)概念的對(duì)稱(chēng)性，