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