Description
Date depot: 6 avril 2021
Titre: Sémantique formelle d'un langage de modélisation du comportement des composants logiciels pour les systèmes de contrôle cyber-physiques
Directeur de thèse:
Jacques MALENFANT (LIP6)
Domaine scientifique: Sciences et technologies de l'information et de la communication
Thématique CNRS : Non defini
Resumé: Dans le cadre d'un projet visant à développer un langage à base de composants pour les systèmes de contrôle cyber-physiques, l'objectif de cette thèse est de concevoir un langage de modélisation du comportement intégré au langage à base de composants puis d'en définir la sémantique formelle. Le langage de modélisation se basera sur les systèmes hybrides stochastiques, capables de capturer à la fois les comportements discrets et continus des systèmes de contrôle cyber-physiques et de l'environnement avec lequel ils interagissent. La sémantique dénotationnelle de ce langage de modélisation sera susceptible d'être combinée par la suite avec une sémantique dénotationnelle de la partie logicielle du composant pour exprimer l'exécution conjointe du logiciel et des modèles. Cette exécution conjointe doit permettre de faire du test, de la vérification, de la validation et de l'adaptation dynamique sûre pour les systèmes de contrôle cyber-physiques.
Résumé dans une autre langue: Part of a larger project aiming at the design and implementation of a component-based programming language for cyber-physical control systems, the objective of this Ph.D. is to design a modeling language integrated with the component-based language and then to define its formal semantics. This modeling language will be based on stochastic hybrid systems, able to capture both the discrete and continuous behaviors of cyber-physical control systems and the environment they interact with. The denotational semantics of this modeling language will foresee its integration with the denotational semantics of the software part of components in such a way to express the joint execution of the models and the software. This joint execution will allow to perform testing, verification, validation, as well as safe dynamic adaptation of cyber-physical control systems.