Verification of reactive systems formal methods and algorithms pdf

Modularity: Complex systems are built from smaller components. Most mod- ern programming languages and hardware description languages therefore pro- vide the concept of modularity. STeP includes facilities for modular specification and verification [FMS98], based on modular transition systems, which can con- cisely describe complex transition systems.

Each module has an interface that determines the observability of module variables and transitions. The interface may also include an environment assumption, a relation over primed and un- primed interface variables that limits the possible environments the module can be placed in. The module can only be composed with other modules that satisfy the environment assumption. Communication between a module and its environ- ment can be asynchronous, through shared variables, and synchronous, through synchronization of labeled transitions.

More complex modules can be constructed from simpler ones by possibly recursive module expressions, allowing the description of hierarchical systems of unbounded depth. Module expressions can refer to modules defined earlier, or instances of parameterized modules, enabling the reuse of code and of properties proven about these modules.

Besides the usual hiding and renaming operations, the language provides a construct to augment the interface with new variables that provide a summary value of multiple variables within the module. Sym- metrically, a restriction operation allows the module environment to combine or rearrange the variables it presents to the module. Real-time and hybrid systems can also be described as modular systems; discrete, real-time and hybrid modules may be combined into one system.

The evolution constraints of hybrid modules may refer to continuous variables of other modules, thus enabling the decomposition of systems into smaller modules.

To enable proofs of nontrivial properties over such modules, we allow arbitrary con- straints on these external continuous variables in the environment assumption. The goal of this compiler is to produce a faithful representation of the input program, taking into account the delays and events that are part of the Verilog semantics.

The compiler extends the Verilog language by allowing parameters to be left unspecified. These parameters can be used to declare bit vectors of arbitrary size, or to compose an array of lower-level modules. These features cater to the deductive component of STeP, which can verify properties of general infinite-state systems. The STeP Session Editor, presented in Figure 3, keeps track of the main properties of interest throughout the verification session, including axioms, assumptions, previously proven properties, and automatically generated invariants, as well as the module to which each applies.

Thus, it can handle multiple systems and proofs simultaneously. Properties can be activated or deactivated to control the extent of their use in automatic theorem-proving. A model of LTL is an infinite sequence of states. We use the usual temporal operators, such as 2p p is always true , 3p p is eventually true , p U q p is true until q is true, which eventually happens , and p W q p awaits q—p is true at least until q is true, but q need not eventually happen. We distinguish between safety and progress properties.

Safety properties do not depend on the fairness constraints of the system, whereas progress properties require the justice or compassion of particular transitions in order to be proved. To specify properties of real-time and hybrid systems, temporal-logic proper- ties can refer to the global and auxiliary clocks, and to the continuous variables; the underlying temporal logic remains the same.

Verification rules reduce temporal properties of systems to first-order verification conditions [MP95]. Verification diagrams [MP94] provide a visual language for guiding, organizing, and display- ing proofs, and automatically generating the appropriate verification conditions as well see Section 4. As clocked and hybrid transition systems are converted into fair transition systems, verification rules and diagrams are uniformly applicable to discrete, real-time and hybrid systems.

However, due to the parameterization of the tick transiton, the resulting verification conditions for real-time and hybrid systems are usually more complex than those for unparameterized discrete systems.

Figure 4 shows the STeP Proof Editor, which is used to apply the basic deduc- tive temporal verification rules as well as the Gentzen-style interactive theorem proving rules.

In a typical deductive verification effort, the top-level goal is a temporal formula to be proven valid for a given system. Verification rules or di- agrams are used to generate verification conditions, as subgoals, which together imply the system validity of the original temporal property.

These subgoals are then established automatically using decision procedures Section 5. Model checking is also initiated by the Proof Editor. STeP Proof Editor depth-first search of the state-space, directed by the temporal tableau automa- ton for the negated specification. Thus, only those states that can potentially violate the specification are visited.

This enables the use of the explicit-state model checker on some infinite-state systems, though it is not guaranteed to terminate for these systems. The symbolic model checker uses a breadth-first search through sets of states represented by ordered binary decision diagrams OBDDs. Thus, it is limited to finite-state systems, whose variables range over a fixed, finite number of values. When transitions can be expressed as guarded commands i.

A specialized backwards search for proving invariants is also available. The set of states visited in the backwards search is constrained by auxiliary invariants, which may have been formulated and verified before, or generated automatically see Section 5. The symbolic and explicit-state model checkers complement each other.

On the other hand, the explicit-state model checker is often faster on systems with relatively few reachable states. Using the notion of modular validity, modular properties can be established by the same set of methods as global properties, accounting for environment transitions. Automatic property inheritance then ensures that such properties can be used as lemmas in proofs over composite modules.

In the case of recursively defined systems, properties can be estab- lished by structural induction. Many properties are not directly guaranteed by a module, but hold only under certain assumptions. Assumptions about the environment can be made when proving a modular property, and subsequently discharged when the module is composed with another. Diagrams can be seen as intermediaries between the system and the property to be proven.

A set of verification conditions is proved, deductively, to show that the diagram faithfully represents computations of the system. An algorithmic check then establishes that the diagram corresponds to the formula being proved.

Together, these two stages show that all computations of the system are models of the temporal property. The STeP Diagram Editor, shown in Figure 5, allows the user to draw a diagram and then prove, using the Proof Editor, the associated verification con- ditions.

In STeP 2. The user can draw an initial version and try to prove the associated verification conditions. If they fail, the user can make local corrections to the diagram or discover something wrong with the system and attempt the proof again. The verification conditions are local to the diagram; failed verification con- ditions point to missing edges or nodes, weak assertions, or possible bugs in the system. Since local changes to a diagram do not affect the verification condi- tions elsewhere, much of the work from the previous iteration can be saved.

STeP Diagram Editor feedback from the Proof Editor, the Diagram Editor can highlight proved and unproved edges and nodes in the diagram, helping the user correct the diagram. A change to the diagram automatically invalidates the verification conditions in the Proof Editor that are affected by the change. Deductive model checking [SUM98] uses diagrams to explore and refine the state-space of possibly infinite-state systems, searching for a counterexample computation by transforming the diagram.

The STeP Diagram Editor supports some of these diagram transformations for interactive state-space exploration. We will include a more comprehensive implementation in upcoming releases. We have developed methods for automatically generating finite-state abstractions of possibly infinite-state systems, using the decision pro- cedures in STeP [CU98, Uri98].

We describe some of these decision procedures in Section 5. The abstraction algorithm compositionally abstracts the transitions of the system, expressed as first-order relations, relative to a given, fixed set of asser- tions which define the abstract state-space.

The number of validity checks is proportional to the size of the system description, rather than the size of the abstract state-space. Once the finite-state abstraction is generated, it can be model checked, explic- itly or symbolically see Section 3. This means that validity at the abstract level implies the validity of the original property over the concrete system; however, if the abstract property fails, the original property might still hold.

In this case, we say that the abstraction was not fine enough. An abstract counterexample can be used, manually, to determine if a corresponding concrete counterexample exists, or else to build a finer abstraction. Both are used extensively in the combinations of deductive and algorithmic verification presented in Sec- tion 4.

Invariant generation is based on approximate propagation, starting from the set of initial states, through the state-space of the system until a fixpoint is reached. Depending on the approximation method used, different types of invariants can be generated: — Local invariants result from analyzing the possible values of individual vari- ables, as well as the relation between control locations and data values.

For real-time and hybrid systems STeP provides an alternative technique of invariant generation, also based on forward propagation of system behavior through the state space, but now starting from the entire state space [BMSU98]. For hybrid systems these techniques have been further optimized to take advantage of the structure of the constraints, resulting in stronger in- variants. In [MS98] we show an example where the invariants thus generated are sufficiently strong to prove the main property of interest.

At the top-level, an algorithm based on congruence closure propagates equality constraints through function symbols. It invokes the other decision procedures as auxiliary simplifiers and solvers. The theories supported in this way include: — Partial orders. Beyond basic equality, partial orders are a more expressive constraint language to specify relations between variables.

Verification conditions involving non- linear arithmetic, which are common in the verification of hybrid systems, are dealt with by techniques that eliminate first- and second-degree variables, as described in [Wei97]. Reasoning about bit-vectors is essential for hardware verifi- cation.

STeP includes decision procedures for fixed-size bit-vectors with boolean bitwise operations and concatenation, and for non-fixed size bit- vectors with concatenation [BP98]. Lists and queues are common data structures, especially in systems using abstract datatypes or asyn- chronous channels. Both lists and queues can be viewed as special cases of words, with concatenation being the basic operation.

Although the known decision procedures for word equalities have prohibitive complexity, the spe- cial cases of lists and queues can be solved efficiently. STeP supports equality reasoning for general recursive datatypes, which allow the specification of S-expressions and other tree-like structures.

Enumeration types and records are treated as special cases of recursive datatypes. Co-inductive data-types, such as lazy lists, are also supported.

Both equality constraints and subterm relationships are supported in the integration of decision procedures. Atomic rela- tions include set equality, inclusion and membership. STeP uses decision procedures not only to check validity, but to simplify formulas as well, rewriting them to smaller, logically equivalent ones.

Efficient formula simplification can make verification conditions more readable and man- ageable, and improves the efficiency of subsequent validity checking. The above decision procedures check validity of ground formulas, where no first-order quantification is present.

STeP extends this combination of ground decision procedures to include theory-specific unification algorithms, which find quantifier instantiations needed for first-order validity checking [BSU97]. As mentioned in Section 3.

An example is the steam boiler case study [ABL96], a benchmark for specification and verification meth- ods for hybrid controlled systems. At the time of its appearance we developed a comprehensive model of this system, including both the plant and the con- troller. The model consisted of some lines of SPL code and contained eight parallel processes. However, verification proved impractical and further analysis was suspended.

Recently the case study was revived. The system was rewrit- ten as a modular transition system consisting of ten modules with a total of 80 transitions, 18 real-valued variables and 28 finite-domain variables. Modularity allowed us to prove properties over selected subsystems and in- herit them for the full system, thus reducing the number of verification condi- tions to be proven.

In some cases, involving discrete finite-state modules only, the model checker could be applied, making the verification fully automatic. In our previous implementation finite-state components could not be separated from the infinite-state ones, and thus use of the model checker was not possible. Assertion-based abstraction see Section 4. The relationships between the relevant real-valued variables captured by a small set of assertions were sufficient to let us prove the properties.

The graphical user interface for STeP 2. The explicit-state model checker is implemented in C, while the symbolic model checker uses ML linked together with external OBDD libraries, written in C.

Similarly, the polyhedral invariant generation uses external polyhedra ma- nipulation routines, implemented in C [HP95]. External systems: Verification conditions in STeP can be output to external theorem provers or decision procedures. STeP interacts with these provers by invoking them in the background and digesting their output to check if the verification conditions have been discharged. Mark Stickel provided AC-unification utilities and feedback.

STeP 2. References [ABL96] J. Abrial, E. Boerger, and H. Since , the author is professor in computer science at the university of Kaiserslautern. This makes it very suitable for a graduate course on selected topics on formal methods. It would also be highly useful as a general reference in logic and automata theory …. I heartily recommend it to every serious formal methods theoretician.

The book is complete with respect to its concepts, and explanations. The research oriented readers can find the book useful …. For theory oriented readers, the flow of chapters is smooth. Skip to main content Skip to table of contents. Advertisement Hide. This service is more advanced with JavaScript available.

Authors view affiliations Klaus Schneider. The book is self-contained Includes all definitions without relying on other material Proves all theorems in detail Covers many formalisms like u-calculus, w-automata, and temporal logics and has special emphasis on the relationship between these formalism Presents detailed algorithms in pseudo-code for verification as well as translations to other formalisms Includes supplementary material: sn.

Pages A Unified Specification Language. Fixpoint Calculi. Finite Automata. Temporal Logics. Predicate Logic. Back Matter Pages