基于模態(tài)邏輯的模型檢測技術(shù)研究.pdf

1、模態(tài)邏輯是邏輯學領(lǐng)域最重要的分支之一。特別是克里普克可能世界語義學的建立，使模態(tài)邏輯有了準確可靠的語義模型，促進了模態(tài)邏輯的快速發(fā)展。模型檢測技術(shù)是形式化驗證領(lǐng)域的重要組成部分，可以對軟硬件系統(tǒng)的正確性進行高度自動化的驗證，在軟件工程領(lǐng)域和工業(yè)界備受矚目。而如何避免狀態(tài)空間爆炸問題、系統(tǒng)性質(zhì)正確描述和長反例理解是模型檢測技術(shù)面臨的三個主要挑戰(zhàn)。如何將模態(tài)邏輯這一強大工具有效地應用到模型檢測技術(shù)中，提高對大型復雜系統(tǒng)進行檢測的能力，從而保

2、證系統(tǒng)的可靠性與安全性是一項意義重大的工作，同時也是理論計算機科學與軟件工程領(lǐng)域的一個重要研究內(nèi)容。針對該課題，本文主要在以下幾個方面進行了研究：
　?。?）提出了一種有限狀態(tài)遷移系統(tǒng)模型的狀態(tài)空間約簡方法。該方法通過適當選取自函子的終結(jié)余代數(shù)，通過模態(tài)邏輯理論中的互模擬等價關(guān)系來產(chǎn)生最小的有限狀態(tài)遷移系統(tǒng)模型。使得該遷移系統(tǒng)能夠完全等價地模擬原遷移系統(tǒng)的所有行為，保證系統(tǒng)驗證的等效性，有效地避免對系統(tǒng)進行模型檢測時的狀態(tài)空間爆炸

3、問題。
　?。?）在Global作用域下構(gòu)造了一類可以正確描述系統(tǒng)性質(zhì)的抽象CTL公式模板。首先，通過對系統(tǒng)性質(zhì)與系統(tǒng)行為進行研究，闡述了以組合命題作為模式與作用域參數(shù)的形式化描述研究的可行性與必要性。然后，通過對線性時序邏輯LTL與分支時序邏輯CTL的研究，給出了用CTL描述系統(tǒng)性質(zhì)的方法。同時，通過重新定義的三個邏輯運算符來簡化公式，使構(gòu)造的CTL公式模板更加簡潔，易于理解。最后，構(gòu)造出 Global作用域下所有模式的CTL公

4、式模板，用來生成由組合命題類、模式和作用域定義的描述系統(tǒng)復雜性質(zhì)和行為的CTL公式。針對所構(gòu)造的CTL公式模板，給出了模板正確性的證明，說明該方法構(gòu)造的CTL公式模板可以生成正確的CTL公式。
　?。?）在Before等作用域下構(gòu)造了可以正確描述系統(tǒng)性質(zhì)的抽象CTL公式模板，從而完善了所有作用域與模式組合的CTL公式模板類。首先，通過對將來區(qū)間邏輯 FIL的語法和語義研究，說明將來區(qū)間邏輯FIL在刻畫系統(tǒng)性質(zhì)和系統(tǒng)行為方面表達能力

5、的不足。特別是對Prospec描述結(jié)果的表示形式上，CTL無疑具有不可替代的優(yōu)勢，而且CTL也是現(xiàn)在眾多優(yōu)秀模型檢測器的輸入語言。然后，通過對系統(tǒng)行為進一步研究，擴展了接受組合命題作為參數(shù)的全部抽象CTL公式模板類，使CTL公式模板構(gòu)造完整化。接著，通過證明得出，所構(gòu)造的CTL公式模板可以正確地產(chǎn)生系統(tǒng)性質(zhì)和行為描述的CTL公式，描述結(jié)果簡潔有效。這些模板可以集成到現(xiàn)有的以CTL為輸入語言的模型檢測器中，作為模型檢測中的系統(tǒng)性質(zhì)描述工具

6、。最后，給出了CTL公式模板的生成實例。
　?。?）提出了一種基于帶權(quán)偶圖演化的不可滿足子式求解算法，用來求解近似最小不可滿足子式。首先，給出了偶圖演化與帶權(quán)偶圖演化定義。然后，分析了不可滿足合取范式的極大可滿足子式與極小不可滿足子式以及與最小不可滿足子式之間的關(guān)系，并給出了它們之間的關(guān)系定理。最后，通過帶權(quán)偶圖演化的數(shù)學模型，給出求解近似最小不可滿足子式的算法，同時給出了該算法正確性的證明與分析。該方法以從無到有的方式自動生成近