Computer Aided Verification

Stålmarck's Method is a patented natural deduction proof method with a novel proof-theoretic notion of proof depth, defined as the largest number of nested assumptions in the proof. An implementation of the method, called Prover, has been used as proof engine in various commercial tools since 1990, and is now integrated in a formal verification framework called NP-Tools. Prover searches for shallow subformula proofs, which has proven to be an efficient strategy for solving many industrial problems, the largest of which today consists of several 100,000's of sub-formulas. Stålmarck's method is in industrial use, for instance in the areas of telecom service specification analysis, analysis of railway interlocking software, analysis of programmable controllers and analysis of aircraft systems. The method seems suitable also for hardware verification.

An abstraction/refinement paradigm for the full propositional μ-calculus is presented. No distinction is made between universal or existential fragments. Necessary conditions for conservative verification are provided, along with a fully automatic symbolic model checking abstraction algorithm. The algorithm begins with conservative verification of an initial abstraction. If the conclusion is negative, it derives a “goal set” of states which require further resolution. It then successively refines, with respect to this goal set, the approximations made in the subformulas, until the given formula is verified or computational resources are exhausted.

We present an approach to designing verified digital systems by a sequence of small local refinements. Refinements in this approach are not limited to a library of predefined transformations for which theorems have been previously established. Rather, the approach relies on localizing the refinement steps in such a way that they can be verified efficiently by model checking. Toward this end, a compositional rule is proposed by which each design refinement may be verified independently, in an abstract environment. This rule supports the use of downward refinement maps, which translate abstract behavior detailed behavior. These maps may involve temporal transformations, including delay. The approach is supported by a verification tool based on symbolic model checking.

When we verify the correctness of an open system with respect to a desired requirement, we should take into consideration the different environments with which the system may interact. Each environment induces a different behavior of the system, and we want all these behaviors to satisfy the requirement. Module checking is an algorithmic method that checks, given an open system (modeled as a finite structure) and a desired requirement (specified by a temporal-logic formula), whether the open system satisfies the requirement with respect to all environments. In this paper we extend the module-checking method with respect to two orthogonal issues. Both issues concern the fact that often we are not interested in satisfaction of the requirement with respect to all environments, but only with respect to these that meet some restriction. We consider the case where the environment has incomplete information about the system; i.e., when the system has internal variables, which are not readable by its environment, and the case where some assumptions are known about environment; i.e., when the system is guaranteed to satisfy the requirement only when its environment satisfies certain assumptions. We study the complexities of the extended module-checking problems. In particular, we show that for universal temporal logics (e.g., LTL, ∀CTL, and ∀CTL*), module checking with incomplete information coincides with module checking, which by itself coincides with model checking. On the other hand, for non-universal temporal logics (e.g., CTL and CTL*), module checking with incomplete information is harder than module checking, which is by itself harder than model checking.

The main obstacle to automatic verification of temporal logic properties of finite-state systems is the state explosion problem. One way to alleviate this is to replace components of a system with smaller ones and verify the required properties from the smaller system. This approach leads to notions of compositional property-preserving equivalences and preorders. Previously we have shown that the NDFD preorder is the weakest preorder which is compositional w.r.t. standard operators and preserves nexttime-less linear temporal logic properties. In this paper we describe a case study where NDFD preorder was used to verify semiautomatically both safety and liveness properties of the Sliding Window protocol for arbitrary channel lengths and realistic parameter values. In this process we located a previously undiscovered fault leading to lack of liveness in a version of the protocol.

In this paper we describe a decision procedure for the core theory of fixed-sized bit-vectors with extraction and composition that can readily be integrated into Shostak's procedure for deciding combinations of theories. Inputs to the solver are unquantified bit-vector equations t=u and the algorithm returns true if t=u is valid in the bit-vector theory, false if t=u is unsatisfiable, and a system of solved equations otherwise. The time complexity of the solver is $$\mathcal{O}\left( {\left| t \right| \cdot log{\text{ }}n + n^2 } \right)$$ , where t is the length of the bit-vector term t and n denotes the number of bits on either side of the equation. Then, the solver for the core bit-vector theory is extended to handle other bit-vector operations like bitwise logical operations, shifting, and arithmetic interpretations of bit-vectors. We develop a BDD-like data-structure called bit-vector BDDs to represent bit-vectors, various operations on bit-vectors, and a solver on bit-vector BDDs.

In this paper, we propose a method for the automatic construction of an abstract state graph of an arbitrary system using the Pvs theorem prover.Given a parallel composition of sequential processes and a partition of the state space induced by predicates ϕ₁, ..., g4 _l on the program variables which defines an abstract state space, we construct an abstract state graph, starting in the abstract initial state. The possible successors of a state are computed using the Pvs theorem prover by verifying for each index i if ϕ_i or ¬ϕ_i is a postcondition of it. This allows an abstract state space exploration for arbitrary programs.

A leak test procedure for a combustion system which is used in the chemical industry was verified. This procedure is important since it reduces the probability of explosions. Both government and internal company standards where employed in creating the initial leak test procedure. Several major faults were discovered by the verification of a logic model of the procedure and equipment using SMV. This paper describes the leak test procedure with its corresponding combustion system pipe network, the approach employed in modeling the process, failure modes included in the process model, computational challenges, and verification results. This study indicates that the formal method, SMV, is an appropriate tool for verification of industrial processes of modest complexity

Hybrid Decision Diagrams (HDD) have been proven in Intel to be an important enabler for the formal verification of datapath intensive circuits and in particular the verification of arithmetic units. However, extensive user interaction with the formal verification tool was required in order to use the HDD technology efficiently. The user had to analyze the circuit and its specification and manually partition the signals and operations into control and datapath.In this paper, we will demonstrate how we have made use of the automatic datapath extraction techniques widely used in the synthesis world in order to efficiently integrate HDDs to an SMV-based formal verification system. The intention of this paper is to illustrate how existing technology can help improve the usability and productivity of the formal verification process and enable efficient integration of new technology, in our case HDDs.The system described in this paper, Prover, statically analyzes the model to be verified and partitions the representation of the logic to HDDs and Binary Decision Diagrams (BDDs). Moreover, the partitioning algorithm decides which vector operations will be represented more efficiently as word-level (i.e. using HDD) versus bit-level (i.e using BDD).The new methodology of integrating HDD into the formal verification process increases the productivity of the verification process. At the same time, experiments with Prover show that verification is (both computation and memory usage wise) as efficient as the previously known manual method.

Binary Decision Diagrams are in widespread use in verification systems for the canonical representation of finite functions. Here we consider multi-valued BDDs, which represent functions of the form $$\varphi :\mathbb{B}^\upsilon \to \mathcal{L}$$ , where $$\mathcal{L}$$ is a finite set of leaves.We study a rather natural online BDD refinement problem: a partition of the leaves of several shared BDDs is gradually refined, and the equivalence of the BDDs under the current partition must be maintained in a discriminator table. We show that it can be solved in O(n log n) if n bounds both the size of the BDDs and the total size of update operations. Our algorithm is based on an understanding of BDDs as the fixed points of an operator that in each step splits and gathers nodes.We apply our algorithm to show that automata with BDD-represented transition functions can be minimized in time O(n·log n), where n is the total number of BDD nodes representing the automaton. This result is not an instance of Hopcroft's classical algorithm for automaton minimization, which breaks down for BDDs because of their path compression property.

Bisimulations that abstract from internal computation have proven to be useful for verification of compositionally defined transition system. In the literature of probabilistic extensions of such transition systems, similar bisimulations are rare. In this paper, we introduce weak bisimulation and branching bisimulation for transition systems where nondeterministic branching is replaced by probabilistic branching. In contrast to the nondeterministic case, both relations coincide. We give an algorithm to decide weak bisimulation with a time complexity cubic in the number of states of the transition system. This meets the worst case complexity for deciding branching bisimulation in the nondeterministic case.

We revisit the approach defined in [2] for the formal verification of cryptographic protocols so as to allow for some mechanization in the verification process. In the original approach verification uses theorem proving. Here we show that for a wide range of practical situations and properties it is possible to perform the verification on a finite and safe abstract model.

We demonstrate the feasibility of using the XSB tabled logic programming system as a programmable fixed-point engine for implementing efficient local model checkers. In particular, we present XMC, an XSB-based local model checker for a CCS-like value-passing language and the alternation-free fragment of the modal mu-calculus. XMC is written in under 200 lines of XSB code, which constitute a declarative specification of CCS and the modal mu-calculus at the level of semantic equations.In order to gauge the performance of XMC as an algorithmic model checker, we conducted a series of benchmarking experiments designed to compare the performance of XMC with the local model checkers implemented in C/C++ in the Concurrency Factory and SPIN specification and verification environments. After applying certain newly developed logic-programming-based optimizations (along with some standard ones), XMC's performance became extremely competitive with that of the Factory and shows promise in its comparison with SPIN.

Parametric timing constraints are expressed naturally in timing diagram logics. Algorithmic verification of parametrically constrained timing properties is a difficult problem known to be undecidable in most general cases. This paper establishes that a class of parametrically constrained timing properties can be verified algorithmically against finite-state systems; alternatively stated containment by a regular language is shown decidable for a class of language properties (regular and non-regular) expressible in our timing diagram logic.

This paper addresses the exact computation of the set of reachable states of a strongly linear hybrid system. It proposes an approach that is an extension of classical state-space exploration. This approach uses a new operation, based on a cycle analysis in the control graph of the system, for generating sets of reachable states, as well as a powerful representation system for sets of values. The method broadens the range of hybrid systems for which a finite and exact representation of the set of reachable states can be computed. In particular, the state-space exploration may be performed even if the set of variable values reachable at a given control location cannot be expressed as a finite union of convex regions. The technique is illustrated on a very simple example.

In this paper we discuss the practical difficulty of analyzing the behavior of timed automata and report some results obtained using an experimental BDD-based extension of KRONOS. We have treated examples originating from timing analysis of asynchronous boolean networks and CMOS circuits with delay uncertainties and the results outperform those obtained by previous implementations of timed automata verification tools.

In [TAKB96], we investigated techniques for checking if one real-time system correctly implements another and developed theory for hierarchical proofs and assume-guarantee style reasoning. In this study, using the techniques of [TAKB96], we verify the correctness of the timing of the communication chip STARI.

Vframe is one of Ansaldo's software driven vital architectures for safety critical products. This paper describes a project whose result is the development of an “embedded verifier”, i.e. a system integrated within Vframe and able to certify the correctness of one of Vframe components, a compiler. The embedded verifier satisfies two precise requirements. First, the compiler must be certified in a fully automatic and efficient way. Second, the embedded verifier must be itself certified, in a way which can be easily understood and validated by end users.

This paper gives an account of the use of model checking in a large-scale microprocessor development project. It describes the tools, methods and techniques used, the way the work was organized, and some of the problems encountered, as well as the results achieved. The verification of a bus arbiter is presented as a case study illustrating the abstraction techniques required in order to achieve results for large designs.

The talk describes the background and motivation for the language of statecharts, discusses some of the semantic issues it raises, shows how statecharts have been embedded in structured-analysis and object-oriented frameworks, and describes the supporting tools, Statemate and Rhapsody, from i-Logix, Inc. Some peripheral research is also mentioned.

An on-the-fly algorithm, for model checking under fairness, is presented. The algorithm utilizes symmetry in the program to reduce the state space, and employs new novel techniques that make the on-the-fly modelchecking feasible. The algorithm uses state symmetry and eliminates paralle edges in the reachability graph. Experimental results, demonstrating dramatic reductions in both the running time and memory usage, are presented.

In this paper we describe the use of symmetry for verification of transistor-level circuits by symbolic trajectory evaluation. We show that exploiting symmetry can allow one to verify systems several orders of magnitude larger than otherwise possible. We classify symmetries in circuits as structural symmetries, arising from similarities in circuit structure, data symmetries, arising from similarities in the handling of data values, and mixed structural-data symmetries. We use graph isomorphism testing and symbolic simulation to verify the symmetries in the original circuit. Using conservative approximations, we partition a circuit to expose the symmetries in its components, and construct reduced system models which can be verified efficiently. We have verified Static Random Access Memory circuits with up to 1.5 Million transistors.

With the use of state and memory reduction techniques in verification by explicit state enumeration, runtime becomes a major limiting factor. We describe a parallel version of the explicit state enumeration verifier Murϕ for distributed memory multiprocessors and networks of workstations that is based on the message passing paradigm. In experiments with three complex cache coherence protocols, parallel Murϕ shows close to linear speedups, which are largely insensitive to communication latency and bandwidth. There is some slowdown with increasing communication overhead, for which a simple yet relatively accurate approximation formula is given. Techniques to reduce overhead and required bandwidth and to allow heterogeneity and dynamically changing load in the parallel machine are discussed, which we expect will allow good speedups when using conventional networks of workstations.

We describe a new heuristic for detecting bad cycles (reachable cycles that are not confined within one or another designated sets of model states), a fundamental operation for model-checking algorithms. It is a variation on a standard implementation of the Emerson-Lei algorithm, which our experimental data suggests can result in a significant speed-up for verification runs that pass. We conclude that this heuristic can be used to advantage on “mature” designs for which the anticipated result of the verification is pass.

Prepositional logic formulas containing implications can suffer from antecedent failure, in which the formula is true trivially because the pre-condition of the implication is not satisfiable. In other words, the post-condition of the implication does not affect the truth value of the formula. We call this a vacuous pass, and extend the definition of vacuity to cover other kinds of trivial passes in temporal logic. We define w-ACTL, a subset of CTL and show by construction that for every w-ACTL formula ϕ there is a formula w(ϕ), such that: both ϕ and w(ϕ) are true in some model M iff ϕ passes vacuously. A useful side-effect of w(ϕ) is that if false, any counter-example is also a non-trivial witness of the original formula ϕ.

We give a linear-time algorithm to translate any formula from computation tree logic (CTL or CTL*) into an equivalent expression in a variable-confined fragment of transitive-closure logic FO(TC). Traditionally, CTL and CTL* have been used to express queries for model checking and then translated into μ-calculus for symbolic evaluation. Evaluation of μ-calculus formulas is, however, complete for time polynomial in the (typically huge) number of states in the Kripke structure. Thus, this is often not feasible, not parallelizable, and efficient incremental strategies are unlikely to exist. By contrast, evaluation of any formula in FO(TC) requires only NSPACE[logn]. This means that the space requirements are manageable, the entire computation is parallelizable, and efficient dynamic evaluation is possible.

We consider the analysis of infinite half-duplex systems which consists of finite state machines that communicate over unbounded channels. The property half-duplex for two machines and two channels (one in each direction) says that each reachable state has at least one channel empty.The contributions of this paper are (a) to give a finite description of the reachability set of such systems, which happens to be effectively recognizable; this description allows us to solve classical verification problems such as: whether a given state is reachable, whether there exist deadlock states, whether the reachability set is finite and whether a specified action is useless; (b) to propose an extension of these results for a new class, systems with quasi-stable channels, which includes systems with similar behavior but which implies more than two machines.

We extend the conventional BDD-based model checking algorithms to verify systems with non-linear arithmetic constraints. We represent each constraint as a BDD variable, using the information from a constraint solver to prune the BDDs by removing paths that correspond to infeasible constraints. We illustrate our technique with a simple example, which has been analyzed with our prototype implementation.

State-space explosion is a central problem in the automatic verification (model-checking) of concurrent systems. Partial order reduction is a method that was developed to try to cope with the state-space explosion. Based on the observation that the order of execution of concurrent (independent) atomic actions is in many cases unimportant for the checked property, it allows reducing the state space by exploring fewer execution sequences. However, to be on the safe side, partial order reductions put constraints about commuting the order of atomic actions that may change the value of propositions appearing in the checked specification. In this paper we relax this constraint, allowing a weaker requirement to be imposed, achieving a better reduction. We demonstrate the benefits of our improved reduction with experimental results.

State space explosion is a fundamental obstacle in formal verification of designs and protocols. Several techniques for combating this problem have emerged in the past few years, among which two are significant: partial-order reductions and symbolic state space search. In asynchronous systems, interleavings of independent concurrent events are equivalent, and only a representative interleaving needs to be explored to verify local properties. Partial-order methods exploit this redundancy and visit only a subset of the reachable states. Symbolic techniques, on the other hand, capture the transition relation of a system and the set of reachable states as boolean functions. In many cases, these functions can be represented compactly using binary decision diagrams (BDDs). Traditionally, the two techniques have been practiced by two different schools—partial-order methods with enumerative depth-first search for the analysis of asynchronous network protocols, and symbolic breadth-first search for the analysis of synchronous hardware designs. We combine both approaches and develop a method for using partial-order reduction techniques in symbolic BDD-based invariant checking. We present theoretical results to prove the correctness of the method, and experimental results to demonstrate its efficacy.

McMillan presented a deadlock detection technique based on unfoldings of Petri net systems. It is realized by means of a backtracking algorithm that has its drawback for unfoldings that increase widely. We present an approach that exploits precisely this property. Moreover, we introduce a fast implementation of McMillan's algorithm and compare it with our new technique.

This paper presents several techniques for formally verifying pipelined microprocessor implementations that contain out-of-order execution and dynamic resolution of data-dependent hazards. Our principal technique models the trace of executed instructions using a table-based representation called a MAETT. We express invariant properties of pipelined implementations by specifying relations between fields in the MAETT. To show the viability of this technique, we have proved the correctness of a simple out-of-order completion pipelined microprocessor design using the ACL2 theorem prover. This verification was performed incrementally by proving that the specified relations hold for all microarchitectural states reachable from a flushed implementation state, eventually permitting us to prove that the entire pipelined machine design implements its ISA specification.

We propose algorithms which combine simulation with symbolic methods for the verification of invariants. The motivation is two-fold. First, there are designs which are too complex to be formally verified using symbolic methods; however the use of symbolic techniques in conjunction with traditional simulation results in better “coverage” relative to the computational resources used. Additionally, even on designs which can be symbolically verified, the use of a hybrid methodology often detects the presence of bugs faster than either formal verification or simulation.

This paper enables symbolic simulation of systems with large embedded memories. Each memory array is replaced with a behavioral model, where the number of symbolic variables used to characterize the initial state of the memory is proportional to the number of memory accesses. The memory state is represented by a list containing entries of the form 〈c, a, d〉, where c is a Boolean expression denoting the set of conditions for which the entry is defined, a is an address expression denoting a memory location, and d is a data expression denoting the contents of this location. Address and data expressions are represented as vectors of Boolean expressions. The list interacts with the rest of the circuit by means of a software interface developed as part of the symbolic simulation engine. The interface monitors the control lines of the memory array and translates read and write conditions into accesses to the list. This memory model was also incorporated into the Symbolic Trajectory Evaluation technique for formal verification. Experimental results show that the new model significantly outperforms the transistor level memory model when verifying a simple pipelined data path.

We present a new symbolic model checker which conservatively evaluates safety and liveness properties on infinite-state programs. We use Presburger formulas to symbolically encode a program's transition system, as well as its model-checking computations. All fixpoint calculations are executed symbolically, and their convergence is guaranteed by using approximation techniques. We demonstrate the promise of this technology on some well-known infinite-state concurrency problems.

In this paper we proposed a formalism based on automata on two dimensional strings for specifying inductive invariants for proving correctness of families of linear and circular networks. We proved our inductive approach to be sound and complete (semantical completeness). We have illustrated our approach by simple examples.We have also given the inductive approach for verification of parametrized systems under fairness. In this case, we use generalized Buchi automata (or Streett automata) as inductive invariants. For this case, we have proved the soundness theorem.As part of future work, it will be interesting to automate the different parts of the induction based approach and apply them to real practical examples. It will also be interesting to extend our approach to networks defined by context free grammars [SG89]. Further more, it will also be interesting to investigate logic based approaches for specification of the invariants.

The paper shows that, by an appropriate choice of a rich assertional language, it is possible to extend the utility of symbolic model checking beyond the realm of BDD-represented finite-state systems into the domain of infinite-state systems, leading to a powerful technique for uniform verification of unbounded (parameterized) process networks.The main contributions of the paper are a formulation of a general framework for symbolic model checking of infinite-state systems, a demonstration that many individual examples of uniformly verified parameterized designs that appear in the literature are special cases of our general approach, verifying the correctness of the Futurebus+ design for all singlebus configurations, extending the technique to tree architectures, and establishing that the presented method is a precise dual to the top-down invariant generation method used in deductive verification.

The PEP tool embeds sophisticated programming and verification components in a user-friendly graphical interface. The basic idea is that the programming component allows the user to design concurrent algorithms in an imperative language, and that the PEP system then generates Petri nets from such programs in order to use Petri net theory for simulation and verification purposes. A key feature is flexibility; its modular design eases the task of adding new interfaces to other verification packages, such as ‘INA’, ‘PROD’ or ‘SMV’.PEP has been implemented on Solaris 2.x, Sun OS 4.1.x and Linux. Ftp-able versions are available via http://www.informatik.uni-hildesheim.de/~pep.

TermiLog is a system implemented in SICStus Prolog for automatically checking termination of queries to logic programs. Given a program and query, the system either answers that the query terminates or that it cannot prove termination. The system can handle automatically 82% of the 120 programs we tested it on.

This work describes Verus, a new tool to be used in the formal verification of realtime systems. In Verus the designer specifies the system to be verified in a C-like language, and uses temporal logic model checking and quantitative timing analysis to verify its correctness. The information produced by our tool can help in verifying a real-time system in many ways. It not only assists in determining its correctness, but also provides insight into the behavior of the system. This allows for a better understanding of the system and in some cases it even suggests optimizations to the design.We have used this tool to analyze several real-time systems of industrial complexity, such as an aircraft controller, a robotics controller and a distributed heterogeneous system. In all cases we have been able to determine the temporal correctness of the system. In several instances the results produced suggested modifications to the design that resulted in more efficient systems.

A hybrid system consists of a collection of digital programs that interact with each other and with an analog environment. Examples of hybrid systems include medical equipment, manufacturing controllers, automotive controllers, and robots. The formal analysis of the mixed digital-analog nature of these systems requires a model that incorporates the discrete behavior of computer programs with the continuous behavior of environment variables, such as temperature and pressure. Hybrid automata capture both types of behavior by combining finite automata with differential inclusions (i.e. differential inequalities). HyTech is a symbolic model checker for linear hybrid automata, an expressive, yet automatically analyzable, subclass of hybrid automata. A key feature of HyTech is its ability to perform parametric analysis, i.e. to determine the values of design parameters for which a linear hybrid automaton satisfies a temporal requirement.

In this paper we present an overview of the verification tool μcke. It is an implementation of a BDD-based μ-calculus model checker and uses several optimization techniques that are lifted from special purpose model checkers to the μ-calculus. This gives the user more expressibility without loosing efficiency.

prod is a reachability analyzer for Predicate/Transition Nets. The tool incorporates several advanced reduced reachability graph generation methods. The tool also includes a CTL model checker and supports on-the-fly verification of LTL formulas. prod is being used in industrial projects at the Digital Systems Laboratory.

VeriSoft is a tool for systematically exploring the state spaces of systems composed of several concurrent processes executing arbitrary code written in full-fledged programming languages such as C or C++. It can automatically detect coordination problems between concurrent processes. Specifically, VeriSoft searches the state space of the system for deadlocks, livelocks, divergences, and violations of user-specified assertions. An interactive graphical simulator/debugger is also available for following the execution of all the processes of the concurrent system.

RuleBase is a symbolic model checking tool, developed by the IBM Haifa Research Laboratory. It is the result of four years of experience in practical formal verification of hardware which, we believe, has been a key factor in bringing the tool to its current level of maturity. Our experience shows that after a short training period, designers can operate the tool independently and achieve impressive results. We present the tool and summarize our development and usage experience, focusing on some work done during 1996.