屈媛媛，杜伊

（四川大學(xué)計(jì)算機(jī)學(xué)院，成都 610065）

軟件模型檢測中狀態(tài)爆炸問題的解決方法

屈媛媛，杜伊

（四川大學(xué)計(jì)算機(jī)學(xué)院，成都 610065）

在軟件模型檢測中，系統(tǒng)所對應(yīng)的狀態(tài)數(shù)會隨著系統(tǒng)大小成指數(shù)級增長，即狀態(tài)空間爆炸問題。為了研究近年來該問題的解決方法，按照系統(tǒng)綜述的方法，歸類整理近年來對近年來解決狀態(tài)空間爆炸的方法，并對每類方法的應(yīng)用、限制以及該領(lǐng)域的未來發(fā)展方向進(jìn)行分析和總結(jié)。

狀態(tài)空間爆炸；模型檢測；文獻(xiàn)綜述

0 引言

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

1 解決狀態(tài)爆炸問題的幾類方法

1.1 偏序約簡

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

1.2 對稱約簡

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

1.3 組合驗(yàn)證方法

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

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

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

1.4 符號化模型檢測方法

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

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

1.5 限界模型檢測方法

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

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

1.6 抽象方法

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

2 結(jié)語

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

[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-），女，四川通江人，研究生，研究方向?yàn)檐浖詣踊瘻y試、模型檢測杜伊（1993-），女，重慶開縣人，在讀碩士研究生，研究方向?yàn)檐浖|(zhì)量保障與測試收稿日期：2016-12-02修稿日期：2017-01-05