SYED-ALWI Syed-Hussein

PhD graduated
Team : ALSOC
Departure date : 07/31/2013

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.

Defence : 07/11/2013

Jury members :

Mme. Laure Petrucci, UPN/LIPN [Rapporteur]
M. Görschwin Fey, Uni. Bremen/DLR [Rapporteur]
Mme. Nihal Pekergin, UP12/LACL
M. Radu Mateescu, CONVECS-INRIA
M. Fabrice Kordon, UPMC/LIP6
Mme. Cécile Braunstein, UPMC/LIP6
Mme. Emmanuelle Encrenaz, UPMC/LIP6

Departure date : 07/31/2013

2012-2014 Publications