Perla TANNOURY : "Développement de CPS, en combinant des modèles SysML, des connecteurs de coordination REO, et des approches formelles"

Résumé : La modélisation et la validation des systèmes cyber-physiques (CPS) présentent des défis significatifs en raison de leur composition hétérogène et de leurs exigences strictes en matière de synchronisation. Ces systèmes intègrent des composants physiques avec des éléments
cybernétiques, interagissant à travers des mécanismes de détection et d'actionnement, ce qui complique le développement de cadres de modélisation unifiés. L'interopérabilité entre les différents composants CPS est cruciale pour la fonctionnalité du système, notamment dans des applications critiques pour la sécurité telles que les systèmes de contrôle des trains. Cette thèse propose un cadre de modélisation CPS complet qui englobe les exigences du système, l'architecture, les protocoles d'interaction et les aspects comportementaux tout en respectant des contraintes strictes de synchronisation. La première contribution introduit "SysReo", un langage de modélisation qui combine SysML et Reo pour soutenir la conception incrémentale des CPS, améliorant la modélisation de la structure du système et la robustesse des protocoles de communication. La deuxième contribution présente une méthode de vérification formelle utilisant les Diagrammes de Séquence SysReo (SysReo SD) pour valider le comportement des CPS par rapport à des propriétés spécifiées, réduisant les erreurs de conception et assurant la correction du système. La troisième contribution introduit "Timed SysReo", qui étend SysML avec Timed Reo pour modéliser les interactions chronométrées dans les CPS, essentielles pour les applications en temps réel telles que les systèmes de lit médical intelligent (SMB). La quatrième contribution présente une approche utilisant les Diagrammes de Séquence Timed SysReo (TSRSD) pour modéliser et vérifier les interactions chronométrées entre les composants CPS, assurant le respect des exigences critiques en matière de synchronisation à l'aide des Automates de Contraintes Chronométrées (TCA) et de la Logique de Flux de Données Programmée Chronométrée (TSDSL). Cette thèse établit une méthodologie robuste pour la modélisation, la conception et la vérification des composants CPS, améliorant la fiabilité et la sécurité du système.

Composition du jury:

M. Ahmed HAMMAD Maîtresse de conférences, Université Bourgogne Franche-Comté, Directeur de thèse
M. Christian ATTIOGBE Professeur des universités Univeristé de Nantes Rapporteur
M. Simon BLIUDZE Chargé de recherche Université de Lille Rapporteur
Mme Rabéa AMEUR-BOULIFA, Professeur des universités Univeristé de Télécom Paris Examinatrice
Mme Olga KOUCHNARENKO, Professeur des universités, Université Bourgogne Franche-Comté Examinatrice
M. Pierre-Cyrille HEAM Professeur des universités, Université Bourgogne Franche-Comté Examinateur

Localisation : Salle des Actes, UFR Sciences et Techniques, 16, Route de Gray