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.

 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  [9] and  [10].

The main elements of our chain are :

  • a front-end for SystemC, called Pinapa, described in [11], 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 VERIMAG + STMicroelectronics common projects [2002...[ for other approaches to the formal validation of SoCs, including runtime verification.

[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 4.2.16 + AHUNTSIC [CC License]

info visites 4141021