- 相關(guān)推薦
計(jì)算機(jī)系統(tǒng)形式化驗(yàn)證中的模型檢測(cè)方法綜述論文
1 形式化方法概述
形式化方法是用數(shù)學(xué)和邏輯的方法來(lái)描述和驗(yàn)證系統(tǒng)設(shè)計(jì)是否滿足需求。它將系統(tǒng)屬性和系統(tǒng)行為定義在抽象層次上，以形式化的規(guī)范語(yǔ)言去描述系統(tǒng)。形式化的描述語(yǔ)言有多種，如一階邏輯，Z語(yǔ)言，時(shí)序邏輯等。采用形式化方法可以有效提高系統(tǒng)的安全性、一致性和正確性，幫助分析復(fù)雜系統(tǒng)并且及早發(fā)現(xiàn)錯(cuò)誤。形式化驗(yàn)證是保證系統(tǒng)正確性的重要方法，主要包括以數(shù)學(xué)、邏輯推理為基礎(chǔ)的演繹驗(yàn)證(deductive verification)和以窮舉狀態(tài)為基礎(chǔ)的模型檢測(cè)(model checking)。演繹驗(yàn)證是基于人工數(shù)學(xué)來(lái)證明系統(tǒng)模型的正確性。它利用邏輯公式來(lái)描述系統(tǒng)，通過(guò)定理或證明規(guī)則來(lái)證明系統(tǒng)的某些性質(zhì)。演繹驗(yàn)證既可以處理有限狀態(tài)系統(tǒng)，又可以解決無(wú)限狀態(tài)問(wèn)題。但是演繹驗(yàn)證的過(guò)程一般為定理證明器輔助，人工參與，無(wú)法做到完全自動(dòng)化，推導(dǎo)過(guò)程復(fù)雜，工作量大，效率低，不能適用于大型的復(fù)雜系統(tǒng)，因而適用范圍較窄。常見(jiàn)的演繹驗(yàn)證工具有HOL，ACL2，PVS和TLV等。模型檢測(cè)主要應(yīng)用于驗(yàn)證并發(fā)的狀態(tài)轉(zhuǎn)換系統(tǒng)，通過(guò)遍歷系統(tǒng)的狀態(tài)空間，對(duì)有限狀態(tài)系統(tǒng)進(jìn)行全自動(dòng)驗(yàn)證，快速高效地驗(yàn)證出系統(tǒng)是否滿足其設(shè)計(jì)期望。下面將主要介紹模型檢測(cè)方法的發(fā)展歷史和研究現(xiàn)狀，以及當(dāng)前面臨的挑戰(zhàn)和未來(lái)發(fā)展方向等問(wèn)題。
2 模型檢測(cè)及相關(guān)技術(shù)
模型檢測(cè)方法最初由Clarke，Emerson等人于1981年提出，因其自動(dòng)化高效等特點(diǎn)，在過(guò)去的幾十年里被廣泛用于實(shí)時(shí)系統(tǒng)、概率系統(tǒng)和量子等多個(gè)領(lǐng)域。模型檢測(cè)基本要素有系統(tǒng)模型和系統(tǒng)需滿足的屬性，其中屬性被描述成時(shí)態(tài)邏輯公式Φ。檢測(cè)系統(tǒng)模型是否滿足時(shí)態(tài)邏輯公式Φ，如果滿足則返回“是”，不滿足則返回“否”及其錯(cuò)誤路徑或反例。時(shí)態(tài)邏輯主要有線性時(shí)態(tài)邏輯LTL(Linear TemporalLogic)和計(jì)算樹邏輯CTL(Computation Tree Logic)。
2.1 線性時(shí)態(tài)邏輯
對(duì)一個(gè)系統(tǒng)進(jìn)行檢測(cè)，重要的是對(duì)系統(tǒng)狀態(tài)正確性要求的形式化，其中一個(gè)基本維度是時(shí)間，同時(shí)需要知道檢驗(yàn)結(jié)果與時(shí)間維度的關(guān)系。使用線性時(shí)態(tài)邏輯(LTL)來(lái)描述系統(tǒng)，可以使得系統(tǒng)更容易被理解，證明過(guò)程更加直截了當(dāng)。LTL公式是一種線性時(shí)態(tài)邏輯。它在表示授權(quán)約束時(shí)，定義了無(wú)限的未來(lái)和過(guò)去，這樣擴(kuò)展了常用語(yǔ)義，并且保證了證明中判定的結(jié)果在各個(gè)時(shí)間點(diǎn)中都是成立的。LTL公式用邏輯連接符和時(shí)態(tài)算子表達(dá)系統(tǒng)運(yùn)行時(shí)狀態(tài)之間的關(guān)系。LTL的邏輯連接符包括：∧(與)，∨ (或)，—|(非)，→(邏輯包含)，←→(邏輯對(duì)等)。時(shí)態(tài)算子包括：G(Globally)，U(Until)，F(xiàn)(Future)，X(neXt-time)。LTL模型檢測(cè)驗(yàn)證系統(tǒng)狀態(tài)轉(zhuǎn)換模型是否滿足屬性，使用可滿足性判定，即為檢測(cè)系統(tǒng)模型M 中是否存在從某個(gè)狀態(tài)出發(fā)的并滿足LTL公式—|Φ 的路徑，如果所有路徑都滿足LTL公式Φ 則不存在有路徑滿足—|Φ。使用LTL公式也有一定的局限性，LTL公式只能包括全稱量詞，對(duì)于混用了全稱和存在量詞的性質(zhì)，一般無(wú)法用這種方法進(jìn)行模型檢測(cè)。
2.2 計(jì)算樹邏輯
計(jì)算樹即為通過(guò)將遷移系統(tǒng)M 某一狀態(tài)作為根，將M 用樹形結(jié)構(gòu)展開(kāi)表示出來(lái)，CTL使用路徑量詞(包括：A(All)，E(Exist))和時(shí)態(tài)算子(包括F，G，X，U)對(duì)計(jì)算樹屬性進(jìn)行形式化的描述，表示出系統(tǒng)的狀態(tài)變化以及狀態(tài)的分枝情況。LTL的時(shí)間定義是與路徑相關(guān)的，每個(gè)時(shí)刻只有唯一的一個(gè)后繼狀態(tài)。LTL可用于有重點(diǎn)的選擇感興趣的路徑分析，并且LTL可以表達(dá)公平概念而CTL不能。但是對(duì)于一些復(fù)雜屬性，如每個(gè)計(jì)算總是可能返回到初始狀態(tài)，LTL將無(wú)法描述，但是CTL可以。CTL的時(shí)間定義是與狀態(tài)相關(guān)的，每個(gè)狀態(tài)都有多個(gè)可能的后繼狀態(tài)，從一個(gè)給定的狀態(tài)量化分離出路徑，能夠斷言行為的存在。CTL可以用路徑量詞E，而LTL不可以;CTL公式使用路徑量詞A時(shí)與LTL公式表達(dá)內(nèi)容可以相同。LTL和CTL各有優(yōu)勢(shì)，Emerson等人提出擴(kuò)展的時(shí)間邏輯CTL，提供了一種統(tǒng)一的框架，包含了LTL和CTL，但是可滿足性判定代價(jià)較高。
2.3 模型檢測(cè)工具
模型檢測(cè)因其自動(dòng)化、高效等特點(diǎn)得到廣泛應(yīng)用，各類模型檢測(cè)工具也層出不窮。以下是幾類典型的模型檢測(cè)工具。SPIN是1980年美國(guó)貝爾實(shí)驗(yàn)室開(kāi)發(fā)的模型檢測(cè)工具，主要關(guān)心系統(tǒng)進(jìn)程間的交互問(wèn)題。它以promela為建模語(yǔ)言，以LTL為系統(tǒng)屬性的邏輯描述語(yǔ)言，支持on-the-fly技術(shù)，可以根據(jù)用戶的需要生成系統(tǒng)的部分狀態(tài)，而無(wú)需構(gòu)建完整的狀態(tài)遷移圖。SPIN驗(yàn)證器無(wú)法驗(yàn)證實(shí)時(shí)系統(tǒng)。NuSMV是1987年由McMillan提出的開(kāi)源的符號(hào)模型檢測(cè)工具。它可以工作于批處理模式，也可以工作于交互模式。NuSMV采用擴(kuò)展的SMV語(yǔ)言描述系統(tǒng)，并用CTL和LTL描述需求。NuSMV結(jié)合了以可滿足性(SAT)為基礎(chǔ)的模型檢測(cè)和以二叉決策樹BDD(Binary Decision Diagram)為基礎(chǔ)的模型檢測(cè)。它具有健壯性，以模塊形式構(gòu)建，不同模塊間無(wú)依賴關(guān)系，代碼易修改。提供了同步模型和異步模型的分區(qū)方法，可以結(jié)合可達(dá)性分析，驗(yàn)證不變性質(zhì)。NuSMV非常靈活，使用者可以控制并且可以改變其系統(tǒng)模塊的執(zhí)行順序，并且可以檢查和修改系統(tǒng)的內(nèi)部參數(shù)來(lái)調(diào)整驗(yàn)證過(guò)程。普通的有限狀態(tài)轉(zhuǎn)換圖無(wú)法模擬動(dòng)態(tài)變化的物理環(huán)境，于是出現(xiàn)了由時(shí)間自動(dòng)機(jī)與有著一系列變量的狀態(tài)轉(zhuǎn)換圖結(jié)合而成的新模型。UPPAAL就是基于這種模型的成熟的實(shí)時(shí)系統(tǒng)驗(yàn)證工具。UPPAAL是1995年由Aallorg大學(xué)和Uppsala大學(xué)共同提出，具有可視化圖形編輯器。它基于時(shí)間自動(dòng)機(jī)并對(duì)其進(jìn)行擴(kuò)展，引入了堅(jiān)定位置、初始化程序、緊迫位置和緊迫管道等概念，有助于對(duì)真實(shí)系統(tǒng)進(jìn)行建模，并能夠有效減少系統(tǒng)內(nèi)存占用。它被用于檢測(cè)不變量和可達(dá)性屬性，尤其是檢測(cè)時(shí)間自動(dòng)機(jī)的控制節(jié)點(diǎn)某些組合以及變量約束是否滿足初始配置。 CPN-Tool是由Aarhut大學(xué)開(kāi)發(fā)的工具，用于有色petri網(wǎng)CPN(Colored Petri Net)的構(gòu)造和分析。有色petri網(wǎng)是用于對(duì)系統(tǒng)進(jìn)行建模并驗(yàn)證其并發(fā)、通信和同步的語(yǔ)言，是一種描述離散事件的圖形化建模語(yǔ)言。它基于meta-language，并有強(qiáng)大的可擴(kuò)展性。它能夠通過(guò)仿真分析系統(tǒng)的行為，通過(guò)模型檢測(cè)驗(yàn)證系統(tǒng)屬性。對(duì)于狀態(tài)爆炸問(wèn)題，CPN-Tool有很多方法來(lái)減少狀態(tài)數(shù)量，Christensen等人使用全局時(shí)鐘和時(shí)間戳作為標(biāo)記，通過(guò)狀態(tài)等價(jià)關(guān)系化簡(jiǎn)狀態(tài)空間，將無(wú)限狀態(tài)轉(zhuǎn)化為有限狀態(tài)。
2.4 狀態(tài)爆炸問(wèn)題
模型檢測(cè)使用狀態(tài)空間檢索來(lái)進(jìn)行系統(tǒng)驗(yàn)證。狀態(tài)空間檢索的主要缺點(diǎn)就是狀態(tài)空間隨著進(jìn)程數(shù)量增CTL使用路徑量詞(包括：A(All)，E(Exist))和時(shí)態(tài)算子(包括F，G，X，U)對(duì)計(jì)算樹屬性進(jìn)行形式化的描述，表示出系統(tǒng)的狀態(tài)變化以及狀態(tài)的分枝情況。
CTL和LTL都有強(qiáng)大的表達(dá)能力。LTL的時(shí)間定義是與路徑相關(guān)的，每個(gè)時(shí)刻只有唯一的一個(gè)后繼狀態(tài)。LTL可用于有重點(diǎn)的選擇感興趣的路徑分析，并且LTL可以表達(dá)公平概念而CTL不能。但是對(duì)于一些復(fù)雜屬性，如每個(gè)計(jì)算總是可能返回到初始狀態(tài)，LTL將無(wú)法描述，但是CTL可以。CTL的時(shí)間定義是與狀態(tài)相關(guān)的，每個(gè)狀態(tài)都有多個(gè)可能的后繼狀態(tài)，從一個(gè)給定的狀態(tài)量化分離出路徑，能夠斷言行為的存在。CTL可以用路徑量詞E，而LTL不可以;CTL公式使用路徑量詞A時(shí)與LTL公式表達(dá)內(nèi)容可以相同。LTL和CTL各有優(yōu)勢(shì)，Emerson等人提出擴(kuò)展的時(shí)間邏輯CTL，提供了一種統(tǒng)一的框架，包含了LTL和CTL，但是可滿足性判定代價(jià)較高。
3 模型檢測(cè)的新進(jìn)展
盡管模型檢測(cè)驗(yàn)證能力在不斷增強(qiáng)，可是對(duì)于復(fù)雜系統(tǒng)的驗(yàn)證仍然面臨許多挑戰(zhàn)。驗(yàn)證混成系統(tǒng)時(shí)，由于其狀態(tài)空間龐大，對(duì)于一些基礎(chǔ)問(wèn)題的驗(yàn)證，具有不可判定性。驗(yàn)證系統(tǒng)的訪問(wèn)控制策略時(shí)，一條策略可能包含大量規(guī)則，如何對(duì)策略建模成為難點(diǎn)。驗(yàn)證多智能系統(tǒng)MAS(Multi-Agent System)時(shí)，由于MAS出現(xiàn)的目的就是用多個(gè)模塊來(lái)解決單一模塊無(wú)法解決的復(fù)雜問(wèn)題，因此MAS的使用環(huán)境一般較為復(fù)雜，行為多樣且具有隨機(jī)性，驗(yàn)證難度較大。本文針對(duì)上述難題，提出一些解決方法如下。驗(yàn)證混合自動(dòng)機(jī)。Krishna等人用混合自動(dòng)機(jī)模型化物聯(lián)網(wǎng)系統(tǒng)，并且用LTL模型檢測(cè)進(jìn)行驗(yàn)證。在使用LTL模型檢測(cè)混合自動(dòng)機(jī)時(shí)，由于LTL具有不可判定性，引入互模擬的概念，并表明一個(gè)有限互模擬的存在意味著使得LTL模型檢測(cè)問(wèn)題的可判定。驗(yàn)證訪問(wèn)控制安全策略。Maarabani等人將組織間模型O2O(Organization to Organization model)與LTL模型相結(jié)合，來(lái)驗(yàn)證互操作訪問(wèn)控制安全策略。將每一個(gè)O2O策略分別用兩個(gè)LTL公式表示，進(jìn)行驗(yàn)證。Hwang，Tao等人定義了一個(gè)新的工具ACPT(Access Control Policy Testing)，將策略制定者的安全需求，轉(zhuǎn)化成可執(zhí)行的策略，并根據(jù)需要對(duì)訪問(wèn)控制策略進(jìn)行動(dòng)態(tài)和靜態(tài)驗(yàn)證驗(yàn)證MAS。Meski等人用基于SAT的限界模型檢測(cè)和基于BDD的限界模型檢測(cè)分別驗(yàn)證多智能系統(tǒng)MAS，并對(duì)兩種驗(yàn)證方法的時(shí)間和內(nèi)存耗費(fèi)方面等進(jìn)行比較。由于目前對(duì)MAS的驗(yàn)證技術(shù)不支持主流驗(yàn)證工具，且輸入形式單一，Hunter等人提出擴(kuò)展驗(yàn)證框架可以支持多種輸入，并且提供翻譯器將輸入翻譯為多個(gè)主流驗(yàn)證工具的輸入語(yǔ)言，利用現(xiàn)有的驗(yàn)證工具對(duì)MAS進(jìn)行驗(yàn)證。由于MAS的使用環(huán)境相對(duì)復(fù)雜，其行為具有隨機(jī)性，Song針對(duì)MAS行為具有隨意性的難題，提出一種概率建模語(yǔ)言對(duì)MAS的進(jìn)行描述，并提出相應(yīng)的模型檢測(cè)框架。
4 結(jié)束語(yǔ)
形式化驗(yàn)證方法已經(jīng)被廣泛的研究，各種描述語(yǔ)言與驗(yàn)證工具層出不窮。相對(duì)于演繹驗(yàn)證，模型檢測(cè)因其全自動(dòng)并可以提供有數(shù)學(xué)基礎(chǔ)的反例等特點(diǎn)，適用范圍更廣，可用于驗(yàn)證軟件、硬件和協(xié)議系統(tǒng)等多個(gè)領(lǐng)域。利用模型檢測(cè)時(shí)需控制好狀態(tài)數(shù)量，進(jìn)行存儲(chǔ)壓縮或者使用必要的路徑壓縮、狀態(tài)縮減算法非常關(guān)鍵。同時(shí)前期對(duì)于保護(hù)目標(biāo)的選取也非常關(guān)鍵，選出關(guān)鍵資產(chǎn)來(lái)保護(hù)可以大大提高后期的描述與驗(yàn)證效率。本文工作可為模型檢測(cè)方法的研究提供借鑒和參考意義。
【計(jì)算機(jī)系統(tǒng)形式化驗(yàn)證中的模型檢測(cè)方法綜述論文】相關(guān)文章：
側(cè)面碰撞中PSM模型的建立與驗(yàn)證04-28
從方法向方法論的綜述分析論文04-30
遺傳檢測(cè)綜述04-27
分析方法的驗(yàn)證05-01
水質(zhì)模型參數(shù)識(shí)別與驗(yàn)證的探討05-01
前瞻記憶的理論模型綜述04-29
水環(huán)境評(píng)價(jià)模型綜述04-26
人員疏散速度模型綜述04-26