Traitement de l'information et modélisation
Ingénierie des systèmes critiques
Conception et évaluation formelle de systèmes critiques
Objectifs
L'objectif des travaux est de développer des moyens formels pour maîtriser la conception et la validation des systèmes critiques en utilisant des méthodes adaptées à chaque niveau de développement et à chaque objectif, pour construire une vision globale formelle optimisée des systèmes et en faisant le lien avec la pratique industrielle en matière de vérification (intégration dans le processus, certification)
Domaines d’application
les domaines d'application sont principalement constitués par les systèmes embarqués pour les transports à différents niveaux de granularité (du logiciel aux systèmes avion).
Contexte
Les systèmes critiques exigent une assurance quant à leur bon fonctionnement qui s'avère cruciale. Il est donc nécessaire de pouvoir établir une démonstration de la correction de ces systèmes en particulier vis à vis des autorités de certification.
L'augmentation de la taille et de la complexité de ces systèmes rendent les opérations de vérification et validation longues et coûteuses voire impossible à faire avec des moyens classiques tels que la simulation et le test.
Par ailleurs un développement multi-facettes caractérise le développement de ces systèmes pour lesquels différents aspects d’un même système sont étudiés par des équipes différentes : Fonctionnel (FXL), Performances Temps Réel (PTR) ou sûreté de fonctionnement (SDF) constituent autant de facettes d'un même système.
Méthodes formelles
Elles font appel à des techniques basées sur les mathématiques pour la spécification, le développement et la vérification de systèmes. Elles permettent en particulier le calcul automatique de propriétés du système. Ce calcul de propriétés permet de fonder une démonstration de correction d'un systèmes. Leur apport réside essentiellement dans le caractère exhaustif et automatiques des preuves opérées. Elles proposent un large éventail de langages et techniques pour les différents types de facettes et d’objectifs de vérification.
