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