| | | Parcours VSC : Modélisation et Validation des Systèmes Critiques |
Présentation
L'application de l'informatique, et en particulier du logiciel, dans des
domaines critiques comme le contrôle/commande temps réel, l'avionique et
les transports, pose évidemment le problème de la validation de ces systèmes.
Ce problème se pose aussi dans les télécommunications, le commerce
électronique, et les systèmes embarqués en général, qui, quoique réputés moins
critiques que les premiers, représentent des enjeux économiques majeurs.
Il s'agit de s'assurer de la sûreté des systèmes (absence d'erreurs, tolérance
aux pannes), mais aussi de leur sécurité (résistance aux attaques,
confidentialité,...).
Ce parcours concerne les méthodes de conception rigoureuse et de validation formelle des systèmes informatiques -- tant logiciels que matériels -- impliqués dans des applications critiques. Ce domaine revêt une importance croissante, et les besoins sont reconnus, concernant tant les developpements de la recherche, que la nécessité de former des ingénieurs spécialistes de ces méthodes.
L'enseignement porte sur les méthodes formelles de conception et
programmation (programmation synchrone, méthodes de dérivation de
programmes), les méthodes de vérification, d'analyse, et de preuve de
programmes (de la théorie à la conception et l'utilisation d'outils)
ainsi que sur les techniques rigoureuses de test.
| Modules | Specialité | ECTS | Volume | Année | |
| DR | Spécification par modèles et développement rigoureux | S&L | 6 | 24h. | impaire |
| VA | Méthodes de vérification automatique | S&L | 6 | 24h. | paire |
| SY | Approche synchrone pour la conception des systèmes réactifs | S&L | 6 | 24h. | impaire |
| MT | Méthodes de test | S&L | 6 | 24h. | paire |
| PP | Preuves et programmes, une introduction à l'aide du système Coq | S&L | 3 | 12h. | impaire |
| SE | Modèles et analyses de protocoles de sécurité | S&L | 3 | 12h. | impaire |
| TH | Systèmes temporisés et hybrides | S&L | 6 | 24h. | paire |
Equipes d'accueil
La recherche dans ce domaine s'effectue principalement dans les équipes
suivantes :
| | | Parcours VSC : Modélisation et Validation des Systèmes Critiques |