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.
- Nicolas Halbwachs
- David Monniaux
- Pascal Raymond
- Matthieu Moy
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.
Program analysis by abstract interpretation is a long-standing research topic in the team, aiming at complementing model-checking techniques with analyses able to take into account numerical properties and data structures. During the considered period, these works took place first within the APRON, and now within the new project ASOPT (static analysis and optimisation) of the ANR programme Arpege (2009-11). In 2007, the arrival of David Monniaux, moving from Patrick Cousot’s team at ENS, was of course a very positive event for this theme.
David Merchat’s thesis was devoted to Cartesian factoring of polyhedra in linear relation analysis (LRA). The results were published in FMSD .
Verification of Array properties
Such analysis is faced with the problem of aliasing: changing a cell A[i] may silently change A[j], if it happens that i = j. As a consequence, we first proposed an analysis deciding whether, at a given program point, two variables are alway different. This was the subject of Mathias Péron’s master thesis  and was published in VMCAI’07 .
Then, we considered the automatic discovery of properties involving array contents, and we proposed an analysis for simple programs (handling one-dimensional arrays by simple iteration), which is able, for instance, to discover that the result of an insertion sort procedure is indeed a sorted array. This was published in PLDI’08 . Moreover, we defined an analysis for discovering that an array is a permutation of another array (which, continuing the previous example, terminates the proof of the sorting procedure: not only the result is sorted, but it is a permutation of the initial array).
Exact abstract fixpoint computation and modular analysis
Two well-known weaknesses of most approaches of static program analysis by abstract interpretation are the computation of fixed points using widen- ings (the classical way of enforcing termination in abstract interpretation) and the lack of modularity.
Concerning widening, it is sometimes possible to compute least fixed points or good approximations thereof directly. In the case of LRA (linear relation analysis) we identified many cases of program loops the abstract effect of which can be computed exactly without iterations: in these cases, the analysis is both more precise and more efficient. Moreover, this technique is compatible with the use of widening, and therefore does not restrict the applicability of the analysis. This work took place in the thesis of Laure Gonnord, and was published in SAS’06 .
Another approach is to reduce the fixed point problem to a quantifier elimination problem (see POPL’09 paper ).
Not only is it possible to exactly solve the least fixed point problem for certain classes of programs and domains, this approach is also modular in the sense that the abstract transfer function of a sub-program can be compiled once and for all. Unfortunately the state of the art in quantifier elimination is not yet satisfactory for this method to scale up well. This led us to work on improvements to quantifier elimination algorithms (see LPAR’08 paper ) based on modern SMT-solving techniques. Another promising direction is to use numerical algorithms from operational research, but these, implemented in floating-point, usually do not provide assurance that their results are correct. We therefore researched how certain floating-point algorithms can be safely applied to accelerate some exact constraint computations (see CAV’09 paper ).
A Complete Verification Chain for SystemC/TLM
Since the PhD of Matthieu Moy, defended at the end of 2005, the group works on a complete verification chain for SystemC/TLM designs. The idea is to perform model extraction from SystemC code, and then to connect to existing verification tools (our model-checker Lesar, SMV and nuSMV, SPIN, and abstract interpretation tools like NBac).
This is different from approaches in which SystemC/TLM models are re-engineered into formal models, to ease the connection to verification tools. In these approaches, the semantics of the SystemC scheduler is changed, and a lot of uncontrollable abstractions are performed. Other approaches based on automatic formal model extraction from real SystemC code include that of  and .
The main elements of our chain are:
- a front-end for SystemC, called Pinapa, described in , and available as an open-source project Pinapa;
- a formalism for the extraction of models from SystemC/TLM, called HPIOM, for heterogeneous Parallel Input-Output machines; systems are described by products of extended synchronous automata;
- the back-ends that connect to SMV, Lesar, etc., from HPIOM.
The full chain is operational, and serves as a proof-of-concept. In particular, Pinapa allows to take any SystemC model into account, which is not the case for other SystemC front-ends. It has been used successfully for industrial case-studies provided by STMicroelectronics.
The verification of a large system-on-a-chip model, taken as a whole, is outside the scope of state-of-the art verification tools. Consequently, we now work on abstractions, component-by-component verification methods, and alternative encodings.
As far as the front-end is concerned, we now look at the SSA (single-static-assignment) form produced by GCC, because previous experiments by the Espresso group at INRIA Rennes have proved that the SSA form can be translated quite naturally into a synchronous formalism. This is one of the research objectives of the FoToVP ANR project (2006-2009) coordinated by Verimag/Synchrone.
See also article 109 and VERIMAG + STMicroelectronics common projects [2002...[ for other approaches to the formal validation of SoCs, including runtime verification.