模態(tài)邏輯是邏輯學(xué)領(lǐng)域最重要的分支之一。特別是克里普克可能世界語義學(xué)的建立,使模態(tài)邏輯有了準(zhǔn)確可靠的語義模型,促進了模態(tài)邏輯的快速發(fā)展。模型檢測技術(shù)是形式化驗證領(lǐng)域的重要組成部分,可以對軟硬件系統(tǒng)的正確性進行高度自動化的驗證,在軟件工程領(lǐng)域和工業(yè)界備受矚目。而如何避免狀態(tài)空間爆炸問題、系統(tǒng)性質(zhì)正確描述和長反例理解是模型檢測技術(shù)面臨的三個主要挑戰(zhàn)。如何將模態(tài)邏輯這一強大工具有效地應(yīng)用到模型檢測技術(shù)中,提高對大型復(fù)雜系統(tǒng)進行檢測的能力,從而保證系統(tǒng)的可靠性與安全性是一項意義重大的工作,同時也是理論計算機科學(xué)與軟件工程領(lǐng)域的一個重要研究內(nèi)容。針對該課題,本文主要在以下幾個方面進行了研究:(1)提出了一種有限狀態(tài)遷移系統(tǒng)模型的狀態(tài)空間約簡方法。該方法通過適當(dāng)選取自函子的終結(jié)余代數(shù),通過模態(tài)邏輯理論中的互模擬等價關(guān)系來產(chǎn)生最小的有限狀態(tài)遷移系統(tǒng)模型。使得該遷移系統(tǒng)能夠完全等價地模擬原遷移系統(tǒng)的所有行為,保證系統(tǒng)驗證的等效性,有效地避免對系統(tǒng)進行模型檢測時的狀態(tài)空間爆炸問題。(2)在Global作用域下構(gòu)造了一類可以正確描述系統(tǒng)性質(zhì)的抽象CTL公式模板。首先,通過對系統(tǒng)性質(zhì)與系統(tǒng)行為進行研究,闡述了...

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

【部分圖文】：

圖1.2L1"L模型檢測算法

Ｆｉｇ．?１．２?Ｔｈｅ?ａｌｇｏｒｉｔｈｍ?ｏｆ?ｍｏｄｅｌ?ｃｈｅｃｋｉｎｇ?ｂａｓｅｄ?ｏｎ?ＬＴＬ??分支時序邏輯ＣＴＬ的各種模型檢測算法［２４ｐ２］采用標(biāo)記法。已，１＞和一個（：１＾公式０，命題連接詞｛丄，＝＾｝構(gòu)成完備集，是時序連接詞的完備集。對于任意給定的ＣＴＬ公式....

圖１．３論文組織結(jié)構(gòu)圖??Ｆｉｇ．?１．３?Ｔｈｅ?ｏｒｇａｎｉｚａｔｉｏｎ?ｏｆ?ｔｈｉｓ?ｔｈｅｓｉｓ??第１章為緒論，對現(xiàn)代模態(tài)邏輯、形式化方法、時態(tài)邏輯與模型檢測以及不可滿足??

定位提供精簡準(zhǔn)確的信息。??１．４論文的組織結(jié)構(gòu)??本文的組織結(jié)構(gòu)如圖１．３所示。??基于模態(tài)邏輯的模型檢測技術(shù)研究??緒論??模型檢測核心內(nèi)容??基于余代數(shù)模?狀態(tài)空間?｜?＾一?近似最小不可滿??態(tài)邏輯方法?｜約簡?丨剛禱?足子式求解方法??形式化描述??ＳＰＳ、Ｐｒｏｓｐｅ....

圖４．１模式的層次關(guān)系圖??Ｆｉｇ．?４．１?Ｔｈｅ?ｈｉｅｒａｒｃｈｙ?ｒｅｌａｔｉｏｎ?ｏｆ?ｐａｔｔｅｒｎ??

到系統(tǒng)性質(zhì)的正確的形式化描述結(jié)果。這些模式之間的層次關(guān)系可以從它們的具體含義??得到。在這些模式中，有的模式需要狀態(tài)／事件發(fā)生，也有的模式不需要狀態(tài)／事件發(fā)生，??如模式的含義。還有的模式具有時序性，如模式的含義。圖４．１給出??了模式的層次關(guān)系。??Ｏｃｃｕｒｒｅｎｃｅ?Ｏｒｄ....

圖４．２作用域選擇樹??Ｆｉｇ．?４．２?Ｔｈｅ?ｃｈｏｉｃｅ?ｔｒｅｅ?ｏｆ?ｓｃｏｐｅ??

第４章Ｂｅ／ｏｒｅ等作用域下系統(tǒng)性質(zhì)描述研宄??表４．１將各模式的層次關(guān)系全面細致的進行闡述和區(qū)分，它是圖４．１的細化與解釋。??通過對表４．１的理解，可以對模式進行更深層次的研宄。從而快速正確的選擇匹配模式，??可以使用恰當(dāng)?shù)哪Ｊ綄ο到y(tǒng)性質(zhì)進行準(zhǔn)確描述。??４．１．２?Ｐｒｏｓ....

本文編號：3928966