命題投影時(shí)序邏輯符號(hào)模型檢測(cè)及其應(yīng)用研究.pdf_第1頁(yè)
已閱讀1頁(yè),還剩128頁(yè)未讀, 繼續(xù)免費(fèi)閱讀

下載本文檔

版權(quán)說(shuō)明:本文檔由用戶提供并上傳,收益歸屬內(nèi)容提供方,若內(nèi)容存在侵權(quán),請(qǐng)進(jìn)行舉報(bào)或認(rèn)領(lǐng)

文檔簡(jiǎn)介

1、模型檢測(cè)是一種驗(yàn)證軟硬件系統(tǒng)、多智能體系統(tǒng)、通信協(xié)議和嵌入式系統(tǒng)等的重要形式化方法。它將待驗(yàn)證系統(tǒng)建模為有限狀態(tài)機(jī),如Kripke結(jié)構(gòu)、狀態(tài)-遷移系統(tǒng)或自動(dòng)機(jī)等,將系統(tǒng)期望的性質(zhì)描述為時(shí)序邏輯公式;然后,自動(dòng)化窮舉搜索系統(tǒng)行為以確定待驗(yàn)證系統(tǒng)是否滿足期望的性質(zhì)。然而,現(xiàn)有模型檢測(cè)方法大多基于顯式狀態(tài)空間描述和操作,即便使用動(dòng)態(tài)狀態(tài)空間構(gòu)建和偏序規(guī)約等優(yōu)化技術(shù),可驗(yàn)證系統(tǒng)的規(guī)模仍然十分有限。在實(shí)際設(shè)計(jì)中系統(tǒng)模型的大小往往隨著并發(fā)組件的數(shù)目

2、呈現(xiàn)指數(shù)級(jí)增長(zhǎng),這一問(wèn)題構(gòu)成了將模型檢測(cè)技術(shù)應(yīng)用于實(shí)際設(shè)計(jì)的主要瓶頸。此外,模型檢測(cè)的形式化規(guī)范語(yǔ)言(如計(jì)算樹邏輯和線性時(shí)序邏輯等)的表達(dá)能力不足,描述順序、并發(fā)和循環(huán)等性質(zhì)較為困難,或者根本無(wú)法描述這些性質(zhì)。因此,本文研究了命題投影時(shí)序邏輯的符號(hào)模型檢測(cè)技術(shù)及其應(yīng)用。
  命題投影時(shí)序邏輯(Propositional Projection Temporal Logic,PPTL)是對(duì)命題區(qū)間時(shí)序邏輯(Propositional

3、Interval Temporal Logic,PITL)的擴(kuò)展。它引入了新的時(shí)序操作符且被證明具有完全正則表達(dá)能力,能夠方便的描述順序、并行、選擇、時(shí)間敏感和周期性等多種并發(fā)的系統(tǒng)性質(zhì)。符號(hào)模型檢測(cè)是一種應(yīng)對(duì)顯式狀態(tài)模型檢測(cè)中容易出現(xiàn)的狀態(tài)空間爆炸問(wèn)題的有效方法。它將待驗(yàn)證系統(tǒng)模型和系統(tǒng)期望的性質(zhì)描述為布爾方程,然后通過(guò)基于規(guī)約有序二叉決策圖的搜索算法查找系統(tǒng)模型中滿足期望性質(zhì)的狀態(tài)集合?;赑PTL和符號(hào)模型檢測(cè)方法的優(yōu)點(diǎn),提出了一

4、個(gè)使用符號(hào)模型檢測(cè)方法驗(yàn)證PPTL規(guī)范的統(tǒng)一框架。在該框架中,將待驗(yàn)證系統(tǒng)建模為Kripke結(jié)構(gòu)M=(S,I,R,L),其中S表示有限狀態(tài)集合,I表示初始狀態(tài)集合,R∈S×S表示集合S上的狀態(tài)遷移關(guān)系,標(biāo)記函數(shù)L用每個(gè)狀態(tài)下成立的原子命題標(biāo)記該狀態(tài);將系統(tǒng)期望的性質(zhì)描述為PPTL公式φ。然后,將期望性質(zhì)的否定形式-φ轉(zhuǎn)化為它對(duì)應(yīng)的范式。由于范式是構(gòu)建標(biāo)記范式圖(Labeled Normal Form Graph,LNFG)的基礎(chǔ),且LN

5、FG包含了目標(biāo)公式所有可能的模型。因此,可以求得狀態(tài)集合Sat-φ,使得對(duì)于該集合中的任意狀態(tài)s,s包含于S且公式-φ在模型M中任何以s開(kāi)頭的路徑上成立。通過(guò)這種方式可以將檢查系統(tǒng)模型M是否滿足期望性質(zhì)φ的問(wèn)題等價(jià)為檢查初始狀態(tài)集合I中滿足?φ的子集SAT(-φ)∩I是否為空的問(wèn)題。事實(shí)上,通過(guò)進(jìn)一步分析發(fā)現(xiàn)PPTL符號(hào)模型檢測(cè)方法的時(shí)間雜度為O{(log|V(φ)|}×|V(φ)|×(|R|+|S|)),其中|V(φ)|為公式φ的LN

6、FG中頂點(diǎn)的數(shù)目,而|R|+|S|表示模型M的大小。此外,通過(guò)驗(yàn)證實(shí)例說(shuō)明了PPTL的符號(hào)模型檢測(cè)方法的可行性。
  基于給出的PPTL符號(hào)模型檢測(cè)方法,本文研究了實(shí)時(shí)與嵌入式計(jì)算系統(tǒng)的形式化驗(yàn)證方法。以單調(diào)速率調(diào)度算法和延遲單調(diào)速率調(diào)度算法為例,驗(yàn)證了上述算法對(duì)任務(wù)集可調(diào)度性的充要條件。將任務(wù)集在單調(diào)速率調(diào)度算法和延遲單調(diào)速率調(diào)度算法調(diào)度下的行為建模為Kripke結(jié)構(gòu),將調(diào)度算法的可調(diào)度性描述為PPTL公式,然后調(diào)用PPTL符號(hào)

7、模型檢測(cè)方法對(duì)任務(wù)集在單調(diào)速率和延遲單調(diào)速率調(diào)度算法下的可調(diào)度性分別進(jìn)行描述和驗(yàn)證。
  近幾年來(lái),基于線性時(shí)序邏輯和分支時(shí)序邏輯的符號(hào)模型檢測(cè)方法是當(dāng)前形式化驗(yàn)證領(lǐng)域最為活躍的研究課題之一,并實(shí)現(xiàn)了相應(yīng)的符號(hào)模型檢測(cè)工具,如SMV、NuSMV和NuSMV2等。但是,上述工具均受制于形式化規(guī)范語(yǔ)言的表達(dá)能力,無(wú)法完整描述順序、并行、選擇、時(shí)間敏感和周期性等性質(zhì)。此外,上述符號(hào)模型檢測(cè)工具均不支持以PPTL公式描述的規(guī)范。因此,本文

溫馨提示

  • 1. 本站所有資源如無(wú)特殊說(shuō)明,都需要本地電腦安裝OFFICE2007和PDF閱讀器。圖紙軟件為CAD,CAXA,PROE,UG,SolidWorks等.壓縮文件請(qǐng)下載最新的WinRAR軟件解壓。
  • 2. 本站的文檔不包含任何第三方提供的附件圖紙等,如果需要附件,請(qǐng)聯(lián)系上傳者。文件的所有權(quán)益歸上傳用戶所有。
  • 3. 本站RAR壓縮包中若帶圖紙,網(wǎng)頁(yè)內(nèi)容里面會(huì)有圖紙預(yù)覽,若沒(méi)有圖紙預(yù)覽就沒(méi)有圖紙。
  • 4. 未經(jīng)權(quán)益所有人同意不得將文件中的內(nèi)容挪作商業(yè)或盈利用途。
  • 5. 眾賞文庫(kù)僅提供信息存儲(chǔ)空間,僅對(duì)用戶上傳內(nèi)容的表現(xiàn)方式做保護(hù)處理,對(duì)用戶上傳分享的文檔內(nèi)容本身不做任何修改或編輯,并不能對(duì)任何下載內(nèi)容負(fù)責(zé)。
  • 6. 下載文件中如有侵權(quán)或不適當(dāng)內(nèi)容,請(qǐng)與我們聯(lián)系,我們立即糾正。
  • 7. 本站不保證下載資源的準(zhǔn)確性、安全性和完整性, 同時(shí)也不承擔(dān)用戶因使用這些下載資源對(duì)自己和他人造成任何形式的傷害或損失。

最新文檔

評(píng)論

0/150

提交評(píng)論