Description
Date depot: 1 janvier 1900
Titre: Vérification formelle des spécifications de systèmes complexes par Réseaux de Petri: application aux Systèmes de Transports Intelligents
Directeur de thèse:
Fabrice KORDON (LIP6)
Domaine scientifique: Sciences et technologies de l'information et de la communication
Thématique CNRS : Non defini
Resumé:
La mise en place de services relatifs à la sécurité sur le réseau routier implique des contraintes de fiabilité qui sont difficiles à satisfaire. Les spécifications de ces systèmes complexes et critiques ont alors un rôle décisif dans la maîtrise de ces contraintes. L’utilisation des méthodes formelles est un moyen efficace pour assister leur conception et leur validation, mais pose encore différents problèmes d’utilisation.
La complexité d’un système rend la tâche de modélisation formelle des spécifications coûteuse, et engendre de l’explosion combinatoire. Aussi, la majorité des techniques de vérification de modèle concerne les systèmes discrets et finis. Or, un grand nombre de propriétés des systèmes complexes reposent sur un ensemble de variables et paramètres continus, on parle alors de système hybrides. La gestion des systèmes hybrides mène souvent à l’élaboration de modèles non finis et sur lesquels il est délicat d’obtenir des résultats d’analyse.
Les projets de développement de systèmes complexes impliquent un grand nombre de partenaires et spécialistes dans des domaines variés. La mise en place du processus de spécification implique une sélection parmi une multitude de méthodes et de formalismes. L’utilisation des méthodes formelles représente alors un coût supplémentaire.
Cette thèse propose de deux contributions complémentaires. D’abord la spécification puis le développement d’une application de sécurité pour la route utilisant les mécanismes de coopération entre l’infrastructure et le conducteur, et les dernières innovations en télécommunication et base de données pour la route.
Ensuite, nous présentons une méthode de la vérification des spécifications de systèmes complexes par modèle checking. Les diagrammes UML sont très répandus dans l’industrie pour la spécification des systèmes complexes. Nous montrons, comment il est possible de les utiliser pour fournir un cadre à l’élaboration de modèles formels.
En définissant un patron formel générique de l’architecture d’un STI, notre méthode offre une solution pour prendre en charge les systèmes complexes. Elle permet modifier des sous parties du modèle formel, sans avoir à modifier le reste du modèle. La définition de règles de transformation des interfaces et des diagrammes d’activités UML vers les réseaux de Petri Symétriques permet de faciliter cette modélisation et d’établir un lien direct entre le modèle formel et les spécifications.
L’intégration de ces phénomènes continus dans des méthodes formelles comme les automates hybrides est un domaine de recherche encore très actif. Nous proposons une solution basée sur la discrétisation de réseaux de Petri Colorés en réseaux Symétriques. La méthodologie présentée offre une solution originale qui traite les problèmes de propagation d’erreurs lors de la discrétisation des aspects continus, et les problèmes d’explosion combinatoires qui y sont liés. Son application au projet de Système de Transport Intelligent SAFESPOT démontre sa capacité à effectuer des analyses formelles impliquant des phénomènes continus.
Doctorant.e: Bonnefoi Fabien