The <b><font color="red">Invariant-Checker</b></font> - Presentation

Presentation

The Invariant-Checker (IC) is a tool for the computer-aided verification developed at VERIMAG laboratory as part of Hassan Saidi's PhD thesis. 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. There are two functionalities of the tool and several auxiliary functionalitites which may be be integrated independently for realising new functionalities:
  1. The Checker functionality is dedicated to the verification of invariance properties of reactive systems using theorem-proving techniques in a systematic ``model checking like'' manner (see also figure 1, below). A system is described as a set of sequential components, each one given by a (set of) transition relation(s) 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' holds 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 automatic (or rarely, assisted) theorem proving.
    In order to prove that a system satisfies an invariance property (expressible by temporal logic formulas of the form ``Always p''), 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. In [MP95] such schemata and corresponding verification rules are presented for other temporal logic formula; notice that STeP (Stanford Temporal Prover) implements such schemata and is built in a similar spirit as our tool.
    Thus, the Checker can be seen as an extension of the PVS specification language to transition systems.
    [GS96] and [Sai97] describe the proof methodology used in this tool.

  2. The Abstractor (see also figure 2, below) is dedicated to predicate abstraction, that is the automatic generation of abstractions of a system to an abstract system using a set of predicates for defining its set of abstract states as described in [GS97] and more recently in [BGL03]. PVS is then used together with a set of strategies to automatically proof that two state sets corresponding to abstract states (valuations of predicates) or state sets are not related via the transition relation. If the proof succeeds; the abstract transition relation does not include such edges, otherwise it does.

    In the Abstractor, we approximate the most general abstraction in two ways.
    (a) As already, stated, we take a safe over approximation, that is if it cannot be proven that two abstract states are unrelated, then they are related. This is common to all tools using the principle of predicate abstraction.
    (b) We consider not any two individual pair of abstract states individually. We compute only successors of reachable states, and consider as potential successor sets only monimials, that is we check the value of the abstract successor set predicate by predicate.
    (c) On the other hand, we reduce the overapproximation by using a number of optimisations exploiting "easily computable facts" in order to reduce the set of reachable states and of potential successors of a given state.

    Most of the successor tools of our Abstractor have chosen different heuristics for efficiently computing abstractions. Most of them, exploit optimisations close to those of (c), but most of them consider abstractions where concrete variables are abstracted individually, that is abstract predicates are built from literals involving only one variable. We do not require such a restriction as our initial aim was, given some system consisting of a set of parallel processes, to constract an abstraction of the global control graph, in order to obtain better results with the Checker (the better the control approximation, the more invariants are inductive invariants, which are those detected by the checker). The obtained abstract state graph can also be analyzed directly by the Aldebaran tool using state exploration of state graphs (note that today Aldebaran is distributed as a module within CADP or IF).

    Abstraction refinement is done starting from a minimization obtained using the Aldebaran tool but is not fully automatized.

  3. In order to simplify, we use an Invariant generator, which implements the static analysis methods described in [BLS96] for deriving control invariants of the syste. In fact, we distinguish facts which must only hold just after a particular transition and invariants and use them differently.

  4. Finally, we use the PVS Type checker to derive "Type checking conditions", which need not to be proven valid formulas but which have to be proven tobe invariants. In addition, they may also be used as auxiliary invariants.

Some 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'=> pretilda[tau](P') is valid for each transition tau of S (where the state predicate pretilda[tau](P) defines Dijkstra's wlp, that is the largest set of states that via the transition relation tau has only successors satisfying P). 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. Nevertheless, for infinite state systems convergence is not guaranteed, and in real life systems with this very simple tactic, convergence is too slow. 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.

Features

The main features of the Inaviant checker are: Also, since the Invariant Checker 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 (TCCS), which are predicates we have to prove as invariants and not as valid formulas. in our case, the TCCS we generate for transition systems represent predicate guaranteeing absence of run-time errors, such as division by zero, application of the tail function on the empty list, etc...
We do not require such TCCS to be valid formulas (as in PVS), but it is enough to prove them to be invariants; notice that they may be used as auxiliary invariants.

Architecture

Figure 1: Invariant verification of SPL programs

Figure 2: Abstraction and refinement with the abstractor

Last modified: Thu Dec 21 13:34:50 MET 2006