軟件模型檢測中狀態爆炸問題的解決方法

屈媛媛，杜伊

（四川大學計算機學院，成都 610065）

軟件模型檢測中狀態爆炸問題的解決方法

屈媛媛，杜伊

（四川大學計算機學院，成都 610065）

在軟件模型檢測中，系統所對應的狀態數會隨著系統大小成指數級增長，即狀態空間爆炸問題。為了研究近年來該問題的解決方法，按照系統綜述的方法，歸類整理近年來對近年來解決狀態空間爆炸的方法，并對每類方法的應用、限制以及該領域的未來發展方向進行分析和總結。

狀態空間爆炸；模型檢測；文獻綜述

0 引言

軟件模型檢測是一組適用于分析和驗證系統行為的自動化技術，其基本框架是構造一個模型，該模型能夠涵蓋系統所達的狀態以及這些狀態之間的轉化，然后驗證這個模型是否滿足系統規格特性。然而，由于系統中存在多個進程，系統所對應的狀態數量會隨著系統的進程數以及進程中的組件數量呈指數增長。這就是所謂的狀態爆炸，是軟件模型檢測在其效率上遇到的主要瓶頸。

1 解決狀態爆炸問題的幾類方法

1.1 偏序約簡

偏序約簡利用并發執行的獨立性，從而忽略一部分狀態[1]。采用拓撲排序過程來解決上述問題,確保偏序約簡的正確性[2]。介紹了兩種偏序約簡的擴展形式用于減小分支安全協議對應的狀態空間大小，一種是約簡后的狀態空間與原始空間具有分支對稱相似性，另一種是約簡后的狀態空間與原始空間具有路徑等價性。本地偏序約簡，該方法基于靜態地計頑固集，其方法實現在模型檢測器Java Pathfinder中。偏序約簡應用有：將本地狀態分析與偏序約簡結合；關注于概率時間自動機，針對具有不確定性的軟件的概率模型；提出將動態偏序約簡和聚集點約簡結合；在驗證概率并發系統時，使用了靜態偏序約簡方法來減小狀態空間；針對并行概率時間自動機提出了新的偏序約簡方法，該方法避免了對狀態的窮盡搜索，只枚舉了一些符號化狀態間激活了的遷移序列；將組合推理驗證方法和偏序約簡相結合。

1.2 對稱約簡

對稱約簡依賴于發現系統的相似進程或組件，交換這些相似進程或組件的執行順序不會影響系統執行的最終結果。弱對稱方法結合了插值以及符號執行來處理這些對稱的狀態，從而緩解狀態爆炸。一種通用的代數方法來探索結構的對稱，該方法并不需要對全局的對稱性有預先的了解，摒棄了對對稱條件符合情況的預先檢查，而是對訪問到的狀態進行動態地標注。使用了靜態偏序約簡，并將該約簡方法使用于動態地采用對稱約簡方法產生的商結構上，實現在了模型檢測工具Modere中[3]。提出了一種更通用的方法，即將對稱約簡以及基于決策圖的狀態符號化表示方法相結合。

1.3 組合驗證方法

組合方法即使用“分而治之”的策略來驗證大型的、復雜的系統[4]。對組合模型檢測方法做出了詳細介紹，并給出了在有限狀態系統、分時系統、概率系統、混成系統使用組合驗證方法緩解狀態爆炸的一些實例。

組合驗證方法大致又分為組合推理和組合最小化。組合推理方法對整個系統的驗證變成了分析系統各個模塊[5]。列舉了一些推理規則或者說策略，包括最為流行的假設/保證規則、演繹規則針對并行系統的組合推理[6]，介紹了一個框架，在這個框架中，多個推理規則都可以被組合并且證明是正確的推理，包括分離邏輯、依賴擔保規則等。將組合推理應用到對實時系統的驗證，結合了不變量演繹規則、可達性分析、線程模塊模型推理對多線程程序進行驗證。

組合最小化方法輸入是系統模型，即用高級語言描述的一組通信的組件。異步系統在組合最小化驗證過程中使用的狀態約簡技術。同步系統在組合最小化過程中一些組件模型約簡技術，這些技術都是基于圖的約簡。

1.4 符號化模型檢測方法

與顯式模型檢測操作單個狀態不同，符號化模型檢測操作的是一組狀態。符號化模型檢測使用布爾方程來表示狀態集和狀態之間的轉化，最常用的數據結構是二元決策圖（BDD）。BDD雖然已經廣泛應用于模型檢測中，但由于其中每個變量的存在量化以及每個布爾運算都會使其大小成指數增長。BDD的大小取決于布爾表達式，以及表達式中變量的順序，這也正符號化模型檢測中也會產生狀態爆炸的根本原因，對BDD的改進主要是OBDD。

在對不確定性系統的驗證方面[7]，針對隨機系統馬爾科夫鏈模型，提出了有效的緩解狀態爆炸的方法，其使用關系代數避免了數值型數據帶來的問題，同時采用互模擬抽象算法來處理純符號型變量。Stateful Timed CSP被廣泛應用于層次化實時系統建模[8]。提出了基于BDD的符號化模型檢測來解決針對該模型檢測可能發生的狀態爆炸問題,主要描述了如何將用Stateful Timed CSP用BDD編碼，該模型檢測方法實現在PAT model checker中。NuSMV是目前最流行的一個基于BDD的符號化模型檢測工具[9]，利用該工具，針對驗證調控網絡，對其中的邏輯管理圖提出了一個符號編碼方法，并考慮了優先類，從而得到一個更小的狀態空間。針對軟件產生線的符號化模型檢測技術，該方法提出了有效的符號表示方法以及啟發式搜索狀態算法。

1.5 限界模型檢測方法

限界模型檢測是符號化模型檢測的補充技術，也是繼其之后解決狀態爆炸的重要突破。限界模型檢測的思想是：將對應的控制流圖以一定的步數展開，然后驗證在這個步數之類是否會達到某個錯誤狀態。例如給定程序P，錯誤狀態E，及步數k，構造一個命題公式看是否滿足在k步之內會達到錯誤狀態E，這個邏輯命題公式可以轉化成SAT實例并通過SAT求解器求解。

Lucas Cordeiro就基于SMT的限界模型檢測編碼做了一系列擴展，使用不同背景的理論和求解器來提高BMC的通過性和精確性，提出了針對多線程嵌入式系統的BMC驗證方法[10]，從SMT求解器中獲取的不滿足信息來對狀態變量和其遷移等數量進行抽象，從而減少狀態空間。該方法的要點在于從SMT求解器中獲取一些證據來控制遷移的數量，從而去除一些與驗證不相關的邏輯[11]。提出了組合驗證來解決驗證嵌入式系統中多線程程序時的狀態爆炸問題，其旨在從配置管理系統中獲取相關信息來自動檢測設計和集成錯誤，系統驗證主要關注新的或修改過的功能，使用等價性檢查來確定是否重新驗證修改后的功能，并結合測試用例來縮小模型檢測器的搜索空間，從而有效地結合了靜態和動態驗證方法。針對大型真實系統驗證的組合限界模型檢測方法，并將其實現在模型檢測工具BLITZ中，該技術結合了近似前置條件及增量化地構造限界模型檢測實例。將限界模型檢測和動態偏序約簡技術相結合來驗證并發程序，這種有界、動態偏序約簡提供了增量覆蓋確保減小狀態空間。

1.6 抽象方法

抽象技術是緩解模型檢測中狀態空間爆炸的一類有效方法，其基本思想是剔除原系統的一些與最終驗證無關的信息，把原有的一組狀態簡化成單個抽象狀態，將原系統映射到一個較小的系統，驗證即針對抽象后的模型，這樣避免了對原始系統建模需要大量的狀態存儲空間。使用計數器抽象技術來減少并行系統中一些不必要的本地狀態。在針對實時系統的組合模型檢測時，利用時間自動機的語義來獲取超近似的抽象，結合了組合抽象和反例引導的抽象精化，并將該方法實現在工具Uppaal中。在針對基于組件模型檢測上，可以使用模塊化的離散抽象方法。針對馬爾可夫決策鏈的、基于隨機兩人游戲的抽象方法，該抽象方法要點在于在原始馬爾科夫鏈的不確定性和抽象后的模型的不確定性之間維護一個缺口/差別。對抽象模型的分析會給出達到一組狀態的最小、最大概率（或期望值）的上界和下界。針對概率模型檢測的組合化抽象還[12]。針對復雜的層次化系統的模型檢測[13]，提出了隨機抽象技術。嵌入式軟件的中斷常會導致模型檢測時發生狀態爆炸，針對這類問題，可以使用基于偏序約簡的抽象技術。參數化系統驗證是指驗證含有不確定數量進程的系統的全局屬性，針對這類驗證問題，聚光燈抽象，該抽象技術利用了對稱參數的概念將系統劃分為焦點進程和影子進程。基于互模擬的抽象來減小檢測模糊時序邏輯模型的狀態空間。

2 結語

本文按照系統文獻綜述方法總結了近5年內解決軟件模型檢測中狀態爆炸方法。近年來最主流的幾類解決狀態爆炸問題的方法。每類方法都有其適用性和局限，上述解決狀態爆炸的幾類主要方法都是可以適當結合應用的，只是一些技術相對簡單，一些技術相對復雜。有研究學者認為使用一些簡單的解決方法都會很有效，相對復雜的技術往往更適用于解決一些特定系統驗證出現的狀態爆炸問題。在一些通用的、主流的模型檢測工具中往往采用的都是一些基礎的技術來解決狀態爆炸，例如狀態空間約簡技術，基礎的技術通用性越強，復雜的技術往往是針對特定的系統。

[1]S.Evangelista，C.Pajault.Solving the Ignoring Problem for Partial Order Reduction.International Journal on Software Tools for Technology Transfer,vol.12,pp.155-170,2010/05/01 2010.

[2]W.Fokkink,M.T.Dashti,A.Wijs.Partial Order Reduction for Branching Security Protocols.in Application of Concurrency to System Design(ACSD),2010 10th International Conference on,2010,pp.191-200.

[3]M.Colange,F.Kordon,Y.Thierry-Mieg,S.Baarir.State Space Analysis Using Symmetries on Decision Diagrams,2012.

[4]K.G.Larsen.Compositional and Quantitative Model Checking(Extended Abstract).in 7th International Andrei Ershov Memorial Conference on Perspectives of System Informatics,PSI 2009,June 15,2009-June 19,2009,Novosibirsk,Russia,2010,pp.35-42.

[5]K.S.Namjoshi,R.J.Trefler.On the Completeness of Compositional Reasoning Methods.1515 Broadway,17th Floor,New York,NY10036-5701,United States,2010.

[6]T.Dinsdale-Young,L.Birkedal,P.Gardner,M.Parkinson,H.Yang.Views:Compositional Reasoning for Concurrent Programs.General Post Office,P.O.Box 30777,NY 10087-0777,United States,2013,pp.287-299.

[7]R.Wimmer,B.Becker.Correctness Issues of Symbolic Bisimulation Computation for Markov Chains.in 15th International GI/ITG Conference on Measurement,Modelling and Evaluation of Computing Systems and Dependability and Fault Tolerance,MMB and DFT 2010,March 15,2010-March 17,2010,Essen,Germany,2010,pp.287-301.

[8]T.K.Nguyen,J.Sun,Y.Liu,J.S.Dong.Symbolic Model-Checking of Stateful Timed CSP using BDD and Digitization.in 14th International Conference on Formal Engineering Methods,ICFEM 2012,November 12,2012-November 16,2012,Kyoto,Japan,2012,pp. 398-413.

[9]P.T.Monteiro,C.Chaouiya.Efficient Verification for Logical Models of Regulatory Networks.in 6th International Conference on Practical Applications of Computational Biology and Bioinformatics,PACBB'12,March 28,2012-March 30,2012,Salamanca,Spain,2012, pp.259-267.

[10]L.Cordeiro.SMT-Based Bounded Model Checking for Multi-Threaded Software in Embedded Systems.Presented at the Proceedings of the 32nd ACM/IEEE International Conference on Software Engineering-Volume 2,Cape Town,South Africa,2010.

[11]G.Basler,M.Mazzucchi,T.Wahl,D.Kroening.Context-Aware Counter Abstraction.Formal Methods in System Design,vol.36,pp. 223-245,2010/09/01 2010.

[12]B.Delahaye,J.-P.Katoen,K.G.Larsen,A.Legay,M.L.Pedersen,F.Sher,et al..Abstract Probabilistic Automata.in 12th Interna-tional Conference on Verification,Model Checking,and Abstract Interpretation,VMCAI 2011,January 23,2011-January 25,2011, Austin,TX,United states,2011,pp.324-339.

[13]A.Basu,S.Bensalem,M.Bozga,B.Delahaye,A.Legay.Statistical Abstraction and Model-Checking of Large Heterogeneous Systems.International Journal on Software Tools for Technology Transfer,vol.14,pp.53-72,2012/02/01 2012.

Methods To Tackle State Explosion in Software Model Checking

QU Yuan-yuan，DU Yi

（Computer College of Sichuan University，Sichuan 610065

For the number of global states of a system with multiple processes can be enormous,it is exponential in both the number of processes and the number of components per process.We map the methods to tackle state space explosion.

State Space Explosion;Software Model Checking;Literature

1007-1423（2017）02-0035-04

10.3969/j.issn.1007-1423.2017.02.009

屈媛媛（1991-），女，四川通江人，研究生，研究方向為軟件自動化測試、模型檢測杜伊（1993-），女，重慶開縣人，在讀碩士研究生，研究方向為軟件質量保障與測試收稿日期：2016-12-02修稿日期：2017-01-05