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

屈媛媛，杜伊

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

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

屈媛媛，杜伊

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

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

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

0 引言

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

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

1.1 偏序約簡(jiǎn)

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

1.2 對(duì)稱(chēng)約簡(jiǎn)

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

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

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

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

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

1.4 符號(hào)化模型檢測(cè)方法

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

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

1.5 限界模型檢測(cè)方法

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

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

1.6 抽象方法

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

2 結(jié)語(yǔ)

本文按照系統(tǒng)文獻(xiàn)綜述方法總結(jié)了近5年內(nèi)解決軟件模型檢測(cè)中狀態(tài)爆炸方法。近年來(lái)最主流的幾類(lèi)解決狀態(tài)爆炸問(wèn)題的方法。每類(lèi)方法都有其適用性和局限，上述解決狀態(tài)爆炸的幾類(lèi)主要方法都是可以適當(dāng)結(jié)合應(yīng)用的，只是一些技術(shù)相對(duì)簡(jiǎn)單，一些技術(shù)相對(duì)復(fù)雜。有研究學(xué)者認(rèn)為使用一些簡(jiǎn)單的解決方法都會(huì)很有效，相對(duì)復(fù)雜的技術(shù)往往更適用于解決一些特定系統(tǒng)驗(yàn)證出現(xiàn)的狀態(tài)爆炸問(wèn)題。在一些通用的、主流的模型檢測(cè)工具中往往采用的都是一些基礎(chǔ)的技術(shù)來(lái)解決狀態(tài)爆炸，例如狀態(tài)空間約簡(jiǎn)技術(shù)，基礎(chǔ)的技術(shù)通用性越強(qiáng)，復(fù)雜的技術(shù)往往是針對(duì)特定的系統(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)檐浖詣?dòng)化測(cè)試、模型檢測(cè)杜伊（1993-），女，重慶開(kāi)縣人，在讀碩士研究生，研究方向?yàn)檐浖|(zhì)量保障與測(cè)試收稿日期：2016-12-02修稿日期：2017-01-05