Direction de recherche : Emmanuelle ENCRENAZ

Co-encadrement : BRAUNSTEIN Cécile

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

Afin d'améliorer la vérification de systèmes synchrones synthétisables, une méthode de vérification par model-checking basée sur une procédure de raffinement d'abstraction s'appuyant sur la structure en composants du système est proposée. Ayant opté pour la génération d'abstraction à partir des propriétés vérifiées des composants, différentes méthodes de sélection de propriétés pour l'abstraction initiale et les stratégies de raffinement pour améliorer le modèle abstrait sont présentées et analysées.
La stratégie la plus directe est la technique de la Négation du Contre-exemple qui raffine le modèle abstrait en éliminant uniquement le contre-exemple fourni par le model-checker. La technique de la sélection de propriété est une autre stratégie où les propriétés disponibles sont organisées en fonction de leur pertinence par rapport à la propriété globale en exploitant les graphes de dépendances de ses variables. De plus, la phase de raffinement est assistée par un mécanisme de filtrage qui assure l'élimination du contre-exemple. Une technique complète basée sur le FSM a également été proposée pour résoudre les principaux problèmes dans l'abstraction dérivée des propriétés, notamment le manque de propriétés exploitables et la génération d'une bonne abstraction.
Les techniques proposées ont été testées sur une plate-forme expérimentale d'un protocole industriel, le bus CAN. Les performances de ces techniques dans la vérification de plusieurs propriétés globales ont été comparées et discutées. Les résultats expérimentaux montrent l'applicabilité des techniques proposées, les gains par rapport aux techniques traditionnelles et l'efficacité relative des trois stratégies proposées varient selon le contexte d'utilisation.

Publications 2012-2014

• 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”, thèse, soutenance 11/07/2013, direction de recherche Encrenaz, Emmanuelle, co-encadrement : 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)