The Invariant Checker - Web Page by Hassen Saidi

Presentation

The Invariant Checker (IC) is a tool for the computer-aided verification dedicated to the verification of invariance properties of reactive systems using a combination of theorem-proving, model-checking and abstract interpretation techniques and tools.
The system is designed as a front-end for the PVS(Prototype Verification System), a theorem prover developed at SRI and based on a variant of type theory. The IC can also be seen as an extension of the PVS specification language to transition systems. The PVS prover is also extended with a proof rule (cf. [MP95]) dedicated to invariance properties. [TOOL-CAV'96] and [TOOL-TACAS'96] describe the proof methodology used in this tool. Additional papers such as [INV-CAV'96] , [CAV'97] and [INFINITY'97] describe some techniques also used. The tool is designed in the spirit of other similar tools such as STeP(Stanford Temporal Prover) .

Objectives

We are interested in using a theorem prover (in our case PVS) in order to verify invariance properties of systems in a systematic ``model checking like'' manner. A system is described as a set of sequential components, each one given by a transition relation and a predicate Init defining the set of initial states. In order to verify that P is an invariant of system S, we try to compute, in an iterative model checking like manner, a predicate P' stronger than P and weaker than Init, and which is an inductive invariant, that is, whenever P' is true in some state , then P' remains true after the execution of any possible transition.
The fact that P' is inductive can be expressed by a set of predicates (having no more quantifiers than P) on the set of program variables, one for every possible transition of the system. In order to prove that P' is inductive, we use either automatic or assisted theorem proving depending on the nature of the formulas to prove.
Our intention is not to verify arbitrary temporal logic formula, but particular formula schemata corresponding to useful property classes. In order to prove that a system satisfies a property, we do not use its semantics, but a proof rule generating a set of predicates such that the validity of these predicates is sufficient to prove the property. Here, we mention only safety properties expressible by formulas of the form ``Always p'' (invariants), where p is a predicate. See [MP95], where many such schemata and corresponding verification rules are presented.

Design choices

This way of dealing with invariant verification differs from the ``classical'' use of theorem proving where program's semantics are encoded in the prover specification language (usually higher order logic or set theory). In this ``classical'' approach the proof process is complicated du to the heavy encoding of semantics and the unnecessary rewriting steps, when rewriting semantics definitions, while usually the most important and difficult part of the verification process is the reasoning about the program variables and their values.
In order to prove that P is an invariant of S (S |= Box P) --- where S is defined by a set of transitions and a predicate Init defining the set of initial states --- it is necessary and sufficient to find a predicate P' weaker than Init and stronger than P which is an inductive invariant, that is P' is preserved by any computational step of S, i.e P'=> \widetilde{pre}[tau](P') (The state predicate \widetilde{pre}[tau](P) defines the smallest set of states that via the transition tau have only successors satisfying P). is valid for each transition tau of S. Model checking consists in computing iteratively the weakest predicate satisfying the proposed solution at each step. This method can be completely automatized under the condition that the above predicates are decidable. However, in the case of infinite state systems convergence is not guaranteed, and in real life systems with this very simple tactic, convergence is too slow, anyway. Convergence can be accelerated by using invariants extracted from the program structure, such as constant propagation, variable domain information, etc. Theorem proving (or an appropriate decision procedure) is used for establishing Q_i => Q_{i+1} that is for verifying that a fixed point has been reached.
In the IC tool a minimal number of verification conditions in a simplified form is generated. Also, automatic generation of auxiliary invariants by static analysis is provided. These predicates are used automatically in the proof of generated VCs. Since the number of this auxiliary invariants is important, we use only the relevant ones to achieve the proof of a VC.
Recently, we added a new feature which consist in the use of abstraction techniques. Given a set of predicates P1,...,Pn, an abstract state graph of a system is constructed in an automatic way. This abstract state graph can be seen as a more precise global control graph from which stronger invariant can be generated. This abstract state graph can also be analyzed by the Aldebaran tool for the state exploration of state graphs.

Features

The main features of the IC tool are: Also, since the IC is built on the top of PVS, its design provides two important features. The first one is the use of the powerful constructions of the PVS specification language, for the description of parallel systems. The second one is the use of the PVS proof checker to discharge verification conditions in an efficient and automatic manner as much as possible. Program variables can be of any type definable in PVS, and can be assigned by any definable PVS expression of the same type. Notice that we allow sub-typing as in PVS, and then typechecking our specification is then undecidable. This requires the generation of type correctness conditions, which are predicates we have to prove as invariants and not as valid formulas. in our case, the tccs we generate for transition systems can just be interpreted as predicate indicating the absence of common run-time errors. such common run-time errors are division by zero, application of the tail function on the empty list, etc... This Tccs can be proved as invariant and used as auxiliary ones. In the case where they can not be proved, we just can not guaranty the absence of a run-time error in the typechecked system.

Architecture

Figure 1



Figure 2



Documentation

A breve tutorial and reference manual is in preparation. It contains the description of the exact syntax for describing transition systems. The different commands to invoke the functions of the system, such as type checking transition systems, generating invariants, invoking the invariance proof rule, and automatic construction of an abstract state graph are also described.

 A short description is available.

Distribution

If you want to play with the tool, please send me an email:
saidi@csl.sri.com

Bibliography

  • H.Saidi. Automated Deductive Verification of parallel Systems. In Proceedings of the Fourth NASA Langley Formal Methods Workshop (Lfm'97), Hampton, Virginia, September 1997.

  • D.Lesens, H.Saidi. Automatic Verification of Parameterized Networks of Processes by Abstraction . In Proceedings of the 2nd International Workshop on the Verification of Infinite State Systems (INFINITY'97), Bologna, Italy, July 1997.

  • S.Graf, H.Saidi. Construction of abstract state graphs with PVS. In Proceedings of the 9th Conference on Computer-Aided Verification (CAV'97), Haifa, Israel, June 1997.

  • H.Saidi. The Invariant-Checker : Automated Deductive Verification of Reactive Systems (Tool Presentation). In Proceedings of the 9th Conference on Computer-Aided Verification (CAV'97), Haifa, Israel, June 1997.

  • S.Graf, H.Saidi. Verifying Invariants Using Theorem Proving. In Proceedings of 8th Conference on Computer-Aided Verification (CAV'96), Rutgers University, New Jersey, July 1996.

  • S.Bensalem, Y.Lakhnech, H.Saidi. Powerful Techniques for the Automatic Generation of Invariants. In Proceedings of 8th Conference on Computer-Aided Verification (CAV'96), Rutgers University, New Jersey, July 1996.

  • H.Saidi A Tool for Proving Invariance Properties of Concurrent Systems Automatically (Tool Presentation). In Proceedings of 2nd International Workshop, Tools and Algorithms for the Construction and Analysis of Systems (TACAS), Passau, Germany, March 1996. Lecture Notes in Computer Science 1055, pages 412--416, Springer-Verlag.

    Related bibliography

  • [MP95] Zohar Manna and Amir Pnueli. Temporal Verification of Reactive Systems: Safety. Springer-Verlag, 1995.

    Case studies

    Examples.

    Verification of a Bounded Retransmission Protocol (BRP).

    Verification Parameterized networks:

    Mux-Ast protocol.

    Fisher's protocol.

    Comments

    Please, send your comments, remarks or suggestions to:


    Hassen Saidi
    Computer Science Laboratory
    SRI International
    333 Ravenswood Ave
    Menlo Park California 94025, USA

    Email: saidi@csl.sri.com

    Tel: 650/859-3810
    Fax: 650/859-2844

    Back to Hassen Saidi home page

    Last modified: Thu Mar 27 14:32:20 MET