Pôle Modèles Modélisation des systèmes critiques

Responsable : Frédéric Boulanger

On s'intéresse au développement de systèmes composés de logiciel en interaction avec un environnement qui comprend du matériel et des humains. De tels systèmes sont qualifiés de critiques quand leur défaillance a des conséquences lourdes sur le matériel ou les humains. Dans ce cas, il est indispensable d'investir dans des méthodes de vérification pour prévenir les défaillances, et les modèles formels permettent de définir correctement ces méthodes.

La modélisation des systèmes considérés fait appel à différents paradigmes, ce qui mène à des modèles hybrides, temporisés, notamment pour les systèmes cyber-physiques qui combinent hybridation et communication.

La vérification de ce type de modèle exige l'utilisation conjointe de différentes méthodes, ce qui implique de combiner la sémantique de ces méthodes d'une manière consistante.

L'aspect critique de ces systèmes impose des contraintes sur la qualité du processus de développement. C'est pourquoi nous modélisons également ces processus afin de pouvoir les certifier, par exemple selon les normes CENELEC 50128, Critères Communs ISO 15408, Do 176c etc. Ces modèles de processus définissent une spécification des méta-données de développement, et permettent de vérifier la conformité du document de développement à cette spécification. Chaque norme définit certains types de méta-données qui sont spécifiées dans une ontologie.

Listes des publications

Mots-clefs : Modèle, Système, Contrôle, Vérification, Validation, Diagnostic, Systèmes cyberphysiques/hybrides/critiques, Ingénierie dirigée par les modèles, Langages spécifiques à un domaine, Sémantique des langages de modélisation

Logiciels : Isabelle/DOF, HOL-CyberPhy, ModHel'X, TESL

Table des matières

Modélisation des Processus de Développement par Ontologies
Un Framework de Modélisation des Systèmes Cyberphysiques
Développement de systèmes complexes utilisant des théories de domaines
Modélisation logique des raisonnements humains
Modélisation multi-paradigme et multi-échelle

Membres de la thématique

Modélisation des Processus de Développement par Ontologies

Participants : Idir AIT-SADOUNE, Achim BRUCKER (Univ. Exeter), Nicolas Meric (phd), Burkhart WOLFF

Suivant l'approche le résultat d'un processus de développement est un document intégré consistant en des étapes Analyse, Conception, Modélisation, Codage et Tests/Vérification, nous avons conçu le système Isabelle/DOF. Isabelle/DOF permet de spécifier des ontologies pour annoter des modèles, λ–termes, preuves, éléments de texte, du code avec des méta-informations. Ceci permet des tests automatiques et continus de la cohérence entre les théories et leurs documents, i.e. la cohérence entre le formel et l’informel. Isabelle/DOF est profondément intégré dans l’écosystème d’Isabelle permettant un aperçu incrémental. Il est intégré dans l'Archive of Formal Proofs (AFP) et disponible dans le developer GIT.

Principales publications

Invited Talk ABZ 2023, IFM 2019, et Science of Computer Programming 2024. Poster disponible

Un Framework de Modélisation des Systemes Cyberphysiques

Participants : Benoît BALLENGHIEN (phd), Paolo Crisafulli (IRT SystemX), Adrien DURIER, Benjamin PUYOBRO (phd), Burkhart WOLFF

Nous avons développé le Framework HOL-CyberPhy sur la base de Isabelle/HOL et la théorie HOL-CSP. HOL-CyberPhy modélise des "acteurs" comme des processus communicants en HOL-CSP, synchronisés par un "demon" qui force les acteurs à certains moments de se synchroniser sur leur état physique (position, vitesse, acceleration, etc...) dans une "scène globale". Le modèle génère donc des series de "snapshots" (traces) bien connues dans les simulateurs des constructeurs d'automobiles, mais permet de raisonner avec des moyens déductifs sur l'ensemble de toutes les traces. Une application du framework est la modélisation des algorithmes non-déterministes de decision des acteurs. Ces algorithmes (des stratégies de conduite) peuvent être analysés et leur safety peut être prouvée en toute généralité. HOL-CyberPhy et différentes applications sous forme des études de cas sont disponible sur notre developer GIT.

Principales publications

Robotics and Autonomous Systems 2023, Poster disponible

Développement de systèmes complexes utilisant des théories de domaines

Participants : Idir AIT-SADOUNE

Un des objectifs principal du projet ANR EBRP, est la définition de mécanismes d'extension pour la méthode Event-B plutôt que des langages de modélisation spécifiques à un domaine. L'extension d'Event-B pour prendre en charge les développements de systèmes complexes nécessitant la modélisation d'objets mathématiques complexes et la prise en charge des preuves associées reste un défi de recherche. L'approche de développement préconisée dans le projet ANR EBRP est expérimentée pour le cas des comportements discrèts et continus. Nous visons la définition de théories de domaine pour gérer le développement de systèmes issus de domaines d'ingénierie différents, comme les systèmes autonomes, et des ontologies de domaine telles que la cybersécurité, le transport, le monde médical, le web sémantique, etc.

Principales publications

MEDI2019 MEDI2023 Rodin2024

Modélisation logique des raisonnements humains

Participants : Frédéric BOULANGER, Safouan TAHA

Afin d'intégrer les comportements humains dans le diagnostic, la surveillance et la simulation des systèmes, nous avons développé un modèle des connaissances d'un agent humain, ainsi qu'un modèle formel de la théorie AGM de révision des connaissances. Ce modèle nous a permis de valider un algorithme de diagnostic des erreurs humaines fondé sur le maintien de la cohérence des connaissances. Ces travaux vont se poursuivre dans le cadre du projet ANR IDEFIX

Poster

Publications

Thèse de Valentin Fouillard, HAR2023, HSMC2021

Modélisation multi-paradigme et multi-échelle

Participants : Frédéric BOULANGER, Burkhart WOLFF, Safouan TAHA

La modélisation de systèmes complexes fait appel à différents paradigmes de modélisation : dynamique continue, événements discrets, automates etc. D'autre part, les différents niveaux d'abstraction auxquels il faut considérer le système pour étudier certaines propriétés entraînent l'utilisation conjointe de plusieurs modèles d'un même système à différentes échelles.

Les correspondances entre les modèles qui utilisent des paradigmes différents, ainsi qu'entre les modèles du système à différentes échelles doivent être bien définies pour que les simulation ou les analyses aient un sens. Un des aspects de ces correspondances est le recollement temporel des différents modèles, qui peut être spécifié en TESL, un langage que nous avons conçu pour synchroniser la simulation de modèles dans l'outil ModHel'X, et dont une sémantique formelle a été développée en Isabelle/HOL.

Ces travaux ont été appliqués dans plusieurs contextes (simulation des smart grids, modélisation qualitative de systèmes cyber-physiques), et sont maintenant appliqués à la modélisation multi-échelle de réseaux ferroviaires pour leur supervision.