Conception et vérification de systèmes critiques
Ref: 2SC5810
Description
Ce cours vise à aborder à la fois la conception et la vérification des systèmes complexes et critiques en utilisant des techniques issues du Génie Logiciel. Les composants de tels systèmes étant hétérogènes (c-à-d. à la fois physiques et logiciels), les méthodologies et les outils présentés dans ce cours seront multiples et s’intègrent dans le cadre d’un cycle de développement. L’idée est de commencer la phase d’analyse en utilisant des outils semi-formels (UML, SysML, ...), souvent utilisés dans l’ingénierie des systèmes pour décrire la structuration du système et ses interactions, puis d’aborder scientifiquement les phases de conception et de validation en utilisant des techniques formelles du Génie Logiciel (modélisation temporisée, stockastique et hybride, logique temporelle, model-checking). L’objectif principal d’une telle démarche vise à montrer, à travers les modèles formels obtenus, que le système fait bien ce que l'on attend de lui tout en respectant les contraintes imposées par le cahier des charges et par l’environnement, ou dans le cas contraire, à extraire les états du système qui peuvent remettre en cause son bon fonctionnement. Dans ce dernier cas, le gain sur le plan économique est très intéressant et appréciable par les ingénieurs qui gagneront à corriger les problèmes détectés par la vérification du modèle avant de passer à l’étape de l’implémentation (programmation).
Numéro de trimestre
ST5
Prérequis
- Système d’information et programmation,
- Algorithmique et complexité,
- Modélisation
Syllabus
- Chapitre 1 - Présentation des logiques temporelles : LTL, CTL
- Chapitre 2 - La vérification avec le Model Checking
- Chapitre 3 - Les automates temporisés : Modélisation et Vérification
- Chapitre 4 - Les modèles stochastiques : Modélisation et Vérification
Composition du cours
- 10,5h de Cours
- 18h de TD : Travaux dirigés
Notation
Examen écrit (1H30)
Ressources
- Marc Aiguier, (Département informatique)
- Idir Ait Sadoune, (Département informatique)
- Paolo Ballarini, (Département informatique)
- Lina Ye (Département informatique)
La langue d'enseignement est le français, mais la majorité des ressources pédagogiques sont écrites en Anglais
Résultats de l'apprentissage couverts par le cours
A la fin de cet enseignement, l’élève sera capable de :
- Modéliser un système à logiciels critiques en utilisant différentes approches formelles (Logique temporelle, Automates, Automates temporisé, modèles stochastiques, automates hybrides).
- Modéliser un système à logiciels critiques en prenant en considération différents types de contraintes (fonctionnelles, non-fonctionnelles, temporelles, ...)
- Analyser scientifiquement le modèle d'un système à logiciels critiques en utilisant des techniques issues du Génie Logiciel (Technique de Vérification formelle : Model Checking).
- Extraire les états d'un système à logiciels critiques qui peuvent remettre en cause son bon fonctionnement.
- Valider le modèle d'un système à logiciels critiques (le système fait bien ce qu'on attend de lui).
Description des compétences acquises à la fin du cours
- C1 - Analyze, design, and build complex systems with scientific, technological, human, and economic components
- C2 - Develop in-depth skills in an engineering field and a family of professions