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
Projects
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.
