Bounded Model Checking Using Satisfiability Solving

The phrase model checking refers to algorithms for exploring the state space of a transition system to determine if it obeys a specification of its intended behavior. These algorithms can perform exhaustive verification in a highly automatic manner, and, thus, have attracted much interest in industry. Model checking programs are now being commercially marketed. However, model checking has been held back by the state explosion problem, which is the problem that the number of states in a system grows exponentially in the number of system components. Much research has been devoted to ameliorating this problem.In this tutorial, we first give a brief overview of the history of model checking to date, and then focus on recent techniques that combine model checking with satisfiability solving. These techniques, known as bounded model checking, do a very fast exploration of the state space, and for some types of problems seem to offer large performance improvements over previous approaches. We review experiments with bounded model checking on both public domain and industrial designs, and propose a methodology for applying the technique in industry for invariance checking. We then summarize the pros and cons of this new technology and discuss future research efforts to extend its capabilities.     

模型检测新技术研究

1 引言软件是否可信赖已成为一个国家的经济、国防等系统能否正常运转的关键因素之一,尤其在一些诸如核反应堆控制、航空航天以及铁路调度等安全悠关(safety-critical)领域更是如此。这类系统要求绝对安全可靠,不容半点疏漏,否则将导致灾难性后果。如1996年6月4日,欧洲航天局阿丽亚娜(Ariane)501火箭因为其控制软件的规范和设计错误而导致发射37秒后爆炸。类似的报道屡见不鲜,如何确保这些系统的可靠性成为计算机科学与控制论领域共同关注的一个焦点问题。     

Automatic verification of concurrent systems using a formula-based compositional approach

When verifying concurrent systems, described by transition systems, state explosion is one of the most serious problems: systems are often described by transition systems with a prohibitive number of states. The primary cause of this problem is the parallel composition of interacting processes. In the recent years, compositional techniques have been developed to attack the state explosion problem. These techniques are based on dividing the verification task into simpler tasks, exploiting the natural decomposition of complex systems into processes. In this paper we present a formula-based compositional approach that allows us to deduce a property of a parallel composition of processes by checking it only on a component process. The approach can be automated and it is completely transparent to the user. Received: 17 May 2001 / 27 February 2002     

一种基于时间自动机的域构造方法

模型检验是一种重要的形式化自动验证技术,通过状态空间搜索来保证软硬件设计的正确性。由于TCTL不是针对时间自动机,而是针对有限状态变迁系统的,从而无法使用TCTL直接对时间自动机进行模型检验。给出了一种从时间自动机到有限状态变迁系统的方法,并在不改变时间自动机的语义上,使时间自动机等价后的域状态数尽可能少,在一定程度上有效地解决了状态空间爆炸问题。     

Abstract reduction in directed model checking CCS processes

Model checking tools face a combinatorial blow up of the state-space (commonly known as the state explosion problem) that must be addressed to formally verify concurrent systems. We propose an approach combining abstraction techniques and heuristic search to overcome the problem above. In particular, heuristic search can avoid the bottleneck of the exhaustive exploration of the global state graph of a system, while retaining the advantages of abstraction techniques.     

一种自动的形式化验证技术-模型检测

模型检测是针对有限状态系统行为的逻辑性质的一种自动验证技术,已有许多工业应用.其主要缺陷是空间爆炸问题.本文通过一简单实例介绍其基本思想、检测步骤和相关理论,给出一些处理状态空间爆炸问题的优化技术,并与其它验证方法进行了比较,最后简单介绍了软件模型检测的新进展.     

Managing the verification trajectory

In this paper we take a closer look at the automated analysis of designs, in particular of verification by model checking. Model checking tools are increasingly being used for the verification of real-life systems in an industrial context. In addition to ongoing research aimed at curbing the complexity of dealing with the inherent state space explosion problem – which allows us to apply these techniques to ever larger systems – attention must now also be paid to the methodology of model checking, to decide how to use these techniques to their best advantage. Model checking “in the large” causes a substantial proliferation of interrelated models and model checking sessions that must be carefully managed in order to control the overall verification process. We show that in order to do this well both notational and tool support are required. We discuss the use of software configuration management techniques and tools to manage and control the verification trajectory. We present Xspin/Project, an extension to Xspin, which automatically controls and manages the validation trajectory when using the model checker Spin. Published online: 18 June 2002     

一种基于离散时间自动机的LTL性质检测工具

模型检测是一种自动完成性质验证的算法过程,在模型检测过程中会遇到状态空间爆炸的问题,即随系统规模的增长状态空间的大小呈指数增长,如何缓解此问题一直是研究者研究的重点.目前利用模型检测方法对线性时序逻辑(LTL)性质进行检测的工具还比较少,且效率都较低.介绍了一种基于离散时间自动机的LTL性质检测工具,采用了在状态空间中存储延迟序列(DS)的技术,对状态进行压缩存储,减小了时间空间的消耗,加快了检测速度.实验表明,该工具的检测效果是不错的,要好于同类工具,如DTSpin.     

Scenario-driven analysis of systems specified through graph transformations

Model checking is one of the most accurate analysis techniques which are used to verify software and hardware systems. However, the analysis of large and complex systems tends to become infeasible since their state spaces easily become too big. Besides well-known abstraction techniques, which may hamper the accuracy of results, in this paper we propose the use of scenario-driven model checking to address and mitigate the state explosion problem. The proposal starts from systems specified through a Graph Transformation (GT) system and it is focused on the analysis of the most significant scenarios. We exploit the modularity of GT systems to reduce the state space by eliminating all the nodes and rules that are not involved in the scenario. Focused analysis also helps concentrate on the most critical behaviors of the system and smooth the risks associated with them. The paper introduces the analysis approach and explains how scenarios (specified in terms of sequence diagrams) can help to reduce the state space. All main concepts are illustrated through a simple application for a travel agency specified as if it were a service-oriented application.     

基于吴方法的符号模型检验

模型检验技术广泛应用于验证并发系统的性质。它的瓶颈一直是内存爆炸问题,将BDD技术引入到模型检验中的方法能有效地缓和状态组合爆炸问题。然而,随着系统规模的增大,BDD的大小仍呈指数增长。吴方法是一种处理多项式的符号计算方法,能有效地求解代数方程组并成功地应用于几何定理机器证明。给出应用吴方法计算表示Kripke结构和CTL公式的多项式的特征列的方法,从而实现对较大规模的系统性质的验证,进一步缓和状态组合爆炸问题。     

Generating Scenarios by Multi-Object Checking

These days, many systems are developed applying various UML notations to represent the structure and behavior of (technical) systems. In addition, for safety critical systems like Railway Interlocking Systems (RIS) the fulfillment of safety requirements is demanded. UML-based Railway Interlocking (UML-based RI) is proposed as a methodology in designing and developing RIS. It consists of infrastructure objects and UML is used to model the system behavior. This design is validated and demonstrated by using simulation with Rhapsody. Automated verification techniques like model checking have become a standard for proving the correctness of state-based systems. Unfortunately, one major problem of model checking is the state space explosion if too many objects have to be taken into account. Multi-object checking circumvents the state space explosion by checking one object at a time. We present an approach to enhance multi-object checking by generating counterexamples in a sequence diagram fashion providing scenarios for model-based testing.     

Automated circular assume-guarantee reasoning

Model checking is a successful approach for verifying hardware and software systems. Despite its success, the technique suffers from the state explosion problem which arises due to the large state space of real-life systems. One solution to the state explosion problem is compositional verification, that aims to decompose the verification of a large system into the more manageable verification of its components. To account for dependencies between components, assume-guarantee reasoning defines rules that break-up the global verification of a system into local verification of individual components, using assumptions about the rest of the system. In recent years, compositional techniques have gained significant successes following a breakthrough in the ability to automate assume-guarantee reasoning. However, automation has been restricted to simple acyclic assume-guarantee rules. In this work, we focus on automating circular assume-guarantee reasoning in which the verification of individual components mutually depends on each other. We use a sound and complete circular assume-guarantee rule and we describe how to automatically build the assumptions needed for using the rule. Our algorithm accumulates joint constraints on the assumptions based on (spurious) counterexamples obtained from checking the premises of the rule, and uses a SAT solver to synthesize minimal assumptions that satisfy these constraints. To the best of our knowledge, our work is the first to fully automate circular assume-guarantee reasoning. We implemented our approach and compared it with established non-circular compositional methods that use learning or SAT-based techniques. The experiments show that the assumptions generated for the circular rule are generally smaller, and on the larger examples, we obtain a significant speedup.     

Heuristics for model checking Java programs

Model checking of software programs has two goals – the verification of correct software and the discovery of errors in faulty software. Some techniques for dealing with the most crucial problem in model checking, the state space explosion problem, concentrate on the first of these goals. In this paper we present an array of heuristic model checking techniques for combating the state space explosion when searching for errors. Previous work on this topic has mostly focused on property-specific heuristics closely related to particular kinds of errors. We present structural heuristics that attempt to explore the structure (branching structure, thread interdependency structure, abstraction structure) of a program in a manner intended to expose errors efficiently. Experimental results show the utility of this class of heuristics. In contrast to these very general heuristics, we also present very lightweight techniques for introducing program-specific heuristic guidance.     

Encoding a process algebra using the Event B method

This paper presents the use of the B technique in its event based definition. We show that it is possible to encode, using Event B, the models (i.e., transition systems) associated to a process algebra with asynchronous semantics. The obtained Event B models consider that the Event B model associated to the left hand side of a BNF rule defining the algebra expressions is refined by a model corresponding to the right hand side of the same rule. The translation rules of each operator of a basic process algebra are given. Then, an example illustrating each translation rule is given. This approach is based on a proof technique and therefore it does not suffer from the state number explosion problem occurring in classical model checking. The interest of this work is the capability to validate user tasks or scenarios when using a given system and particularly a critical system. Finally, we discuss the application of this approach for validating user interfaces tasks in the human–computer interaction area.     

The effect of uncontrolled concurrency on model checking

Correctness of concurrent software is usually checked by techniques such as peer code reviews or code walkthroughs and testing. These techniques, however, are subject to human error, and thus do not achieve an in‐depth verification of correctness. Model‐checking techniques, which can systematically identify and verify every state that a system can enter, are a powerful alternative method for verifying concurrent systems. However, the usefulness of model checking is limited because the number of states for concurrent models grows exponentially with the number of processes in the system. This is often referred to as the ‘state explosion problem.’ Some processes are a central part of the software operation and must be included in the model. However, we have found that some exponential complexity results due to uncontrolled concurrency introduced by the programmer rather than due to the intrinsic characteristics of the software being modeled. We have performed tests on multimedia synchronization to show the effect of abstraction as well as uncontrolled concurrency using the Promela/SPIN model checker. We begin with a sequential model not expected to have exponential complexity but that results in exponential complexity. In this paper, we provide alternative designs and explain how uncontrolled concurrency can be removed from the code. Copyright © 2007 John Wiley & Sons, Ltd.     

SAT-Solving the Coverability Problem for Petri Nets

Net unfoldings have attracted great attention as a powerful technique for combating state space explosion in model checking, and have been applied to verification of finite state systems including 1-safe (finite) Petri nets and synchronous products of finite transition systems. Given that net unfoldings represent the state space in a distributed, implicit manner the verification algorithm is necessarily a two step process: generation of the unfolding and reasoning about it. In his seminal work McMillan (K.L. McMillan, Symbolic Model Checking. Kluwer Academic Publishers, 1993) showed that deadlock detection on unfoldings of 1-safe Petri nets is NP-complete. Since the deadlock problem on Petri nets is PSPACE-hard it is generally accepted that the two step process will yield savings (in time and space) provided the unfoldings are small.In this paper we show how unfoldings can be extended to the context of infinite-state systems. More precisely, we show how unfoldings can be constructed to represent sets of backward reachable states of unbounded Petri nets in a symbolic fashion. Furthermore, based on unfoldings, we show how to solve the coverability problem for unbounded Petri nets using a SAT-solver. Our experiments show that the use of unfoldings, in spite of the two-step process for solving coverability, has better time and space characteristics compared to a traditional reachability based implementation that considers all interleavings for solving the coverability problem.     

Syntactic reductions for efficient deadlock analysis

A well‐known problem in the verification of concurrent systems based on model checking is state explosion: concurrent systems are often represented by automata with a prohibitive number of states. A reduction technique to reduce state explosion in deadlock checking is presented. The method is based on an automatic syntactic simplification of a calculus of communicating systems (CCS) specification, which keeps the parts of the program structure that may lead to a deadlock and deletes the other parts. Copyright © 2002 John Wiley & Sons, Ltd.     

Abstraction for model checking multi-agent systems

Model checking multi-agent systems (MAS) always suffers from the state explosion problem. In this paper we focus on an abstraction technique which is one of the major methods for overcoming this problem. For a multi-agent system, we present a novel abstraction procedure which reduces the state space by collapsing the global states in the system. The abstraction is automatically computed according to the property to be verified. The resulting abstract system simulates the concrete system, while the universal temporal epistemic properties are preserved. Our abstraction is an overapproximation. If some universal temporal epistemic property is not satisfied, then we need to identify spurious counterexamples. We further show how to reduce complex counterexamples to simple structures, i.e., paths and loops, such that the counterexamples can be checked and the abstraction can be refined efficiently. Finally, we illustrate the abstraction technique with a card game.     

A symbolic model checking approach to verifying satellite onboard software

This paper discusses the use of symbolic model checking technology to verify the design of an embedded satellite software control system called the attitude and orbit control system (AOCS). This system is mission critical because it is responsible for maintaining the attitude of the satellite and for performing fault detection, isolation, and recovery decisions. An executable AOCS implementation by Space Systems Finland has been provided in Ada source code form, and we use the input language of the symbolic model checker NuSMV 2 to model the implementation at a detailed level. We describe the modeling techniques and abstractions used to alleviate the state space explosion due to the handling of timers and the large number of system components controlled by the AOCS. The required behavior has been specified as extended state machine diagrams and translated to temporal logic properties. Besides well-known LTL and CTL model checking algorithms, we adapt a previously unexplored form of the liveness-to-safety approach to the problem. The latter new technique turns out to successfully prove all desired properties of the system, outperforming both the LTL and CTL implementations of NuSMV 2.     

Compositional encoding for bounded model checking

Verification techniques like SAT-based bounded model checking have been successfully applied to a variety of system models. Applying bounded model checking to compositional process algebras is, however, a highly non-trivial task. One challenge is that the number of system states for process algebra models is not statically known, whereas exploring the full state space is computationally expensive. This paper presents a compositional encoding of hierarchical processes as SAT problems and then applies state-of-the-art SAT solvers for bounded model checking. The encoding avoids exploring the full state space for complex systems so as to deal with state space explosion. We developed an automated analyzer which combines complementing model checking techniques (i.e., bounded model checking and explicit onthe-fly model checking) to validate system models against event-based temporal properties. The experiment results show the analyzer handles large systems.