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

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

【部分圖文】：

圖1.2L1"L模型檢測(cè)算法

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

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

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

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

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

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

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

本文編號(hào)：3928966