Formal Verification, Theory, Techniques and Tools

Model-Checking, Abstract-Interpretation

The work on formal verification includes model-checking techniques, and abstract-Interpretation techniques. Lesar is a symbolic or enumerative model-checker for Lustre. NBac is an abstract interpretation tool developed by B. Jeannet during his PhD in the group. Recent work on abstract interpretation techniques includes the verification of the properties of imperative algorithms that depend on the contents of arrays, and general theory for abstract interpretation.

The "Formal Verification" topic used to be one of the main topics of the Synchrone team. There is now a separate team PACS led by David Monniaux on the topic.

 People involved

  • Nicolas Halbwachs
  • David Monniaux
  • Pascal Raymond
  • Matthieu Moy


— openTLM

 Model-checking and abstract interpretation for safety properties

Synchronous observers for the description of safety properties

All our verification tools are based on the use of synchronous observers, to describe both the property to be checked and the assumptions on the program environment under which these properties are intended to hold : an observer of a safety property is a program, taking as inputs the inputs/outputs of the program under verification, and deciding (e.g., by emitting an alarm signal) at each instant whether the property is violated.

Running in parallel with the program, an observer of the desired property, and an observer of the assumption made about the environment one has just to check that either the alarm signal is never emitted (property satisfied) or the alarm signal is emitted (assumption violated), which can be done by a simple traversal of the reachable states of the compound program.

Apart from only needing to consider reachable states (instead of paths) this specification technique has several advantages :
— observers may be written in the same language as the program under verification
— observers are executable, which means they can be tested, or even kept in the actual implementation (redundancy, autotest).

Safety versus liveness properties

Using Lustre, one can only write safety properties, i.e., program invariants. Expressing general temporal properties (liveness) requires sophisticated formalisms such as temporal logics and Büchi automata. Such formalisms allow us to speak about the unbounded future (liveness properties), which is not the case of Lustre. The choice of restricting ourselves to such properties is motivated by the following arguments.

— Safety properties are simple and natural to express, because they can always be written as "Always Prop"

— They are compatible with abstractions :

Abs(Prog) |= Abs(prop) => Prog |= prop ;

and performing such abstractions is absolutely mandatory if one wants to deal with programs and properties involving numerical values (which is generally the case for Lustre programs).

— 99 % of interesting properties are safety properties.

— Even properties that look like liveness properties are actually safety properties. For instance, "the train will stop" is often useless. What we mean is "the train will stop before the wall", which can be rewritten as a safety property ; this is often called a bounded liveness.

Tools : model-checking, abstract interpretation, theorem-proving

— Lesar is a symbolic, BDD-based, model-checker for Lustre. Lesar being a model-Checker, verification is performed on an abstract (finite) model of the program. Concretely, for purely logical programs the proof is complete, whereas in general (in particular when numerical values are involved) the proof is only partial. To get the tool see here.

— NBac is a safety property verification tool, that analyzes synchronous and deterministic reactive systems containing combination of Boolean and numerical variables. NBac is based on the theory of abstract interpretation, which allows us to overcome the undecidability of the reachability/co-reachability problem for the class of programs treated by NBac. Sets of states are represented by values belonging to an abstract domain, and (fix-point) computations are performed. This leads to conservative results : if a state is shown unreachable (resp. not co-reachable), then it is for sure. More details here.

— Gloups is an automatic generator of PVS proof obligations. The tool performs a reduction of the initial property expressed upon finite and infinite sequences into a set of scalar properties : our leading principle for this reduction is (continuous) induction. More precisely, properties are expressed as Lustre observers (programs), and then reduced into a set of scalar proof obligations which are discharged into the PVS theorem prover. An (interactive) proof of these obligations is a proof of the initial invariant.

Those tools have been used with several industrial case studies from EADS (Ariane), Airbus, Schneider, etc. You can find more details here.

[1N. Halbwachs, D. Merchat, and L. Gonnord. Some ways to reduce the space dimension in polyhedra computations. Formal Methods in System Design, 29(1):79-­95, 2006.

[2M. Péron. IS, un domaine numérique abstrait pour l’analyse de programmes manipulant des adresses. Master thesis, Université Joseph Fourier, June 2005

[3M. Péron and N. Halbwachs. An abstract domain extending difference-bound matrices with disequality constraints. In B. Cook and A. Podelski, editors, 8th International Conference on Verification, Model- checking, and Abstract Intepretation, VMCAI’07, Nice, France, 2007.

[4N. Halbwachs and M. Péron. Discovering properties about arrays in simple programs. In ACM Conference on Programming Language Design and Implementation, PLDI 2008, pages 339-­348, Tucson (Az.), 6 2008

[5L. Gonnord and N. Halbwachs. Combining widening and acceleration in linear relation analysis. In 13th International Static Analysis Symposium, SAS’06, Seoul, Korea, 2006

[6David Monniaux. Automatic modular abstractions for linear constraints. In POPL (Principles of programming languages). ACM, 2009

[7David Monniaux. A quantifier elimination algorithm for linear real arithmetic. In LPAR (Logic for Programming Artificial Intelligence and Reasoning), volume 5330 of Lecture Notes in Computer Science, pages 243-­257. Springer Verlag, 2008

[8David Monniaux. On using floating-point computations to help an exact linear arithmetic decision procedure. In Computer-aided verification (CAV), volume 5643 of Lecture Notes in Computer Science, pages 570-­583. Springer Verlag, 2009

[9P. Herber, J. Fellmuth, and S. Glesner. Model checking SystemC designs using timed automata. In CODES/ISSS ’08, pages 131-­136, New York, NY, USA, 2008. ACM.

[10B. Niemann and C. Haubelt. Formalizing TLM with communicating state machines. In Forum on specification & Design Languages (FDL), pages 285-­293, 2006.

[11M. Moy, F. Maraninchi, and L. Maillet-Contoz. The extraction tool for SystemC descriptions of systems-on-a-chip. In EMSOFT, New-York, USA, Sept. 2005.

Contact | Plan du site | Site réalisé avec SPIP 3.1.13 + AHUNTSIC [CC License]

info visites 1699979