Détails sur le séminaire

Résumé : Dans le cadre de cette thèse, on s'intéresse à la vérification formelle des propriétés de sûreté pour les systèmes temps-réels à base de composants.
Le but est de proposer une alternative aux techniques d’exploration où le produit de tous les composants d’un système donné est calculé, résultant en une complexité exponentielle de vérification rendant souvent impossible la vérification de larges systèmes.
La vérification compositionnelle a pour but d’alléger la complexité de vérification d’un système donné en comptant sur l‘analyse locale de ses composants. Les propriétés globales en sont ensuite déduites.
Dans le cas des systèmes temps-réels, une difficulté majeure pour le développement d’une approche compositionnelle est relative au modèle synchrone du temps où les horloges des différents composants avancent simultanément. Cet aspect est, pourtant, difficile à considérer dans un cadre compositionnel.
Nous proposons une méthode basée sur l’approche déductive et consistant à calculer d’une manière purement compositionnelle une sur-approximation de l’ensemble des états atteignables du système à travers un invariant.
Ce dernier se compose d’invariants locaux propres aux composants, un invariant d’interaction caractérisant les interactions entre les composants. En plus, afin de considérer le modèle synchrone du temps, nous introduisons des horloges auxiliaires appelées « Horloges d’Histoire ». Elles permettent de générer des invariants supplémentaires permettant de détecter des relations induites par les synchronisations temporelles des différents composants. Appliqué à plusieurs exemples de
systèmes, l’invariant s’est avéré souvent suffisamment fort avec une réduction importante
de la complexité de vérification.
Toutefois, puisque la méthode est basée sur une sur-approximation, des faux contre-exemples peuvent être générés. Nous avons complété la méthode avec un module destiné pour leur analyse.
Au delà de son passage à l’échelle, la méthode est étendue pour la vérification uniforme des systèmes paramétrés, où certains composants sont identiques. La validité de la propriété peut être affirmée indépendamment de leur nombre.
Cette méthode est implémentée dans l’outil RTD-Finder destiné à la vérification des systèmes modélisés au langage BIP (Behavior-Interaction-Priority).
Les résultats d’expérimentation montrent la réduction de la complexité de vérification en comparaison avec l’approche monolithique, surtout quand l’invariant global est en mesure
de détecter la propriété d’intérêt.



Jury:
Prof. Ahmed Bouajjani
Université Paris Diderot, Rapporteur
Prof. Kim Guldstrand Larsen
Université D’Aalborg , Rapporteur
Prof. Erika Ábrahám
Université de RWTH Aachen , Examinateur
Prof. Florence Maraninchi
Université Grenoble Alpes et INP Grenoble , Examinateur
Prof. Doron Peled
Université de Bar Ilan, Examinateur
Dr. Natarajan Shankar SRI International, Examinateur
Prof. Saddek Bensalem,
Université Grenoble Alpes, Directeur de thèse
Dr. Marius Bozga
Ingénieur de recherche - HDR, CNRS, Co-Directeur de thèse