软件模型检测中状态爆炸问题的解决方法

屈媛媛，杜伊

（四川大学计算机学院，成都 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