Supervision : Emmanuelle ENCRENAZ

Co-supervision : BRAUNSTEIN Cécile

Vérification compositionnelle pour la conception sure de systèmes embarqués

In the aim of improving the verification of synthesizable synchronous systems, a model-checking method based on the abstraction-refinement procedure which relies on the compositional structure of the system is proposed. Having opted for the abstraction generation from verified component properties, different methods of property selection for the initial abstraction and the refinement strategies to improve the abstract model are presented and analyzed.
The most straightforward strategy is the Negation of the Counterexample Technique which refines the abstract model by eliminating exclusively the spurious counterexample provided by the model checker. The Property Selection Technique is another abstraction-refinement strategy where the available properties are ordered according to their relevance towards the global property by exploiting the dependency graphs of its variables. Furthermore, the refinement phase is assisted by a filtering mechanism that ensures the current counterexample will be eliminated. A comprehensive FSM-based technique has also been proposed to address the main problems in property based abstraction in compositional verification notably the lack of exploitable properties and the generation of a good abstraction.
The techniques proposed have been tested on an experimental platform of an industrial protocol, the Controller Area Network (CAN). The performance of these techniques in the verification of several global properties have been compared and discussed. The experimental results demonstrate the applicability of the techniques proposed, the gains in comparison to conventional techniques and the relative effectiveness of the three strategies proposed varies according to the application context.

2012-2014 Publications

• 2014
  • S.‑H. Syed‑Alwi, E. Encrenaz : “FSM-based properties and abstraction of components”, IEEE International Symposium on Rapid System Prototyping, New Delhi, India, pp. 37-43, (IEEE) (2014)
• 2013
  • S.‑H. Syed‑Alwi : “Vérification compositionnelle pour la conception sure de systèmes embarqués”, thesis, phd defence 07/11/2013, supervision Encrenaz, Emmanuelle, co-supervision : Braunstein, Cécile (2013)
  • S.‑H. Syed‑Alwi, C. Braunstein, E. Encrenaz : “Efficient Refinement Strategy Exploiting Component Properties in a CEGAR Process”, chapter in Models, Methods and Tools for Complex Chip Design, selected contributions from FDL 2012, vol. 265, Lecture Notes in Electrical Engineering, pp. 17-36, (Springer) (2013)
• 2012
  • S.‑H. Syed‑Alwi, C. Braunstein, E. Encrenaz : “AN EFFICIENT REFINEMENT STRATEGY EXPLOITING COMPONENT PROPERTIES IN A CEGAR PROCESS”, Forum on specification & Design Languages (FDL 2012), Vienne, Austria, pp. 27-34 (2012)