Détails sur le séminaire

Résumé : Les systèmes cyber-physiques sont une classe de systèmes complexes, de grande échelle, souvent critiques enlever de sûreté, qui apparaissent dans des applications industrielles variées. Des approches de vérification formelle sont capable de fournir des garanties pour la performance et la sûreté de ces systèmes. Elles nécessitent trois éléments: un modèle formel, une méthode de vérification, ainsi qu'un ensemble de spécifications formelles. En revanche, les modèles industriels sont typiquement informels, ils sont analysés dans des environnements de simulation informels et leurs spécifications sont décrites dans un langage naturel informel. Dans cette thèse, nous visons à faciliter l'intégration de la vérification formelle dans le processus industriel de la conception basée sur modèle.
Notre première contribution clé est une méthodologie de transformation de modèle. A partir d'un modèle de simulation standard, nous le transformons en un modèle de vérification équivalent, plus précisément en un réseau d'automates hybrides. Pour cette classe de modèle formel, des algorithmes d'atteignabilité peuvent être appliqués pour vérifier des propriétés de sûreté. Le processus de transformation prend en compte les différences de syntaxe, de sémantique et d'autres aspects de la modélisation. L'un des obstacles rencontré est que des algorithmes d'atteignabilité passent à l'échelle pour des modèles affines par morceaux, mais pas pour des modèles non linéaires. Pour obtenir des surapproximations affines par morceaux des dynamiques non linéaires, nous proposons une technique compositionnelle d'hybridisation syntaxique. Le résultat est un modèle très compact qui retient la structure modulaire du modèle d'origine de simulation, tout en évitant une explosion du nombre de partitions.
La seconde contribution clé est une approche pour encoder des spécifications formelles riches de façon à ce qu'elles puissent être interprétées par des outils d'atteignabilité. Nous prenons en compte des spécifications exprimées sous forme d'un gabarit de motif (pattern template), puisqu'elles sont proches du langage naturel et peuvent être comprises facilement par des utilisateurs non experts. Nous fournissons (i) des définitions formelles pour des motifs choisis, qui respectent la sémantique des automates hybrides, et (ii) des observateurs qui encodent les propriétés en tant qu'atteignabilité d'un état d'erreur. En composant ces observateurs avec le modèle formel, les propriétés peuvent être vérifiées par des outils standards de vérification qui sont automatisés.
Finalement, nous présentons une chaîne d'outils semi-automatisée ainsi que des études de cas menées en collaboration avec des partenaires industriels.



Monsieur Goran FREHSE Professeur, ENSTA ParisTech - U2IS, Directeur de thèse
Madame Thao DANG Directrice de Recherche, CNRS - Verimag, Co-Directrice de thèse
Monsieur Benoît CAILLAUD Directeur de Recherche, Inria Rennes, IRISA, Rapporteur
Monsieur Laurent FRIBOURG Directeur de Recherche, LSV - ENS Cachan, CNRS, Rapporteur
Monsieur Alexandre CHAPOUTOT Professeur, ENSTA ParisTech - U2IS, Examinateur