Sujet : Vérification symbolique et abstraction automatique de systèmes critiques hétérogènes

Responsable : André Arnold   ---   Encadrants : Frédéric Herbreteau & Grégoire Sutre
Téléphone : 05 40 00 33 36
e-mail : frederic.herbreteau@labri.fr, gregoire.sutre@labri.fr
Site Web : http://www.labri.fr/~sutre
Equipe : Modélisation, Vérification et Test de Systèmes Informatisés (MVTsi)

Présentation du sujet :

Le caractère critique de nombreuses applications industrielles, telles que les systèmes de supervision, requiert de s'assurer de leur bon fonctionnement. Celles-ci manipulent des données infinies hétérogènes (par ex. des valeurs analogiques provenant de capteurs, des octets reçus sur un port de communication) que les méthodes classiques de vérification ne peuvent pas toutes manipuler.

Des techniques de vérification symbolique d'une part, et d'abstraction / raffinement d'autre part, ont été développées récemment pour certaines classes de systèmes infinis homogènes. L'une comme l'autre ne permet pas, en général, d'analyser des systèmes complexes hétérogènes de grande taille (systèmes réels).

L'objectif de cette thèse est de combiner ces deux approches afin de pouvoir traiter automatiquement des systèmes issus du monde industriel. Cela passe par l'obtention de techniques symboliques pour des modèles hétérogènes, par l'enrichissement des méthodes d'abstraction, ainsi que par l'intégration des deux approches.

Mot-clés : sûreté des systèmes critiques, vérification formelle, systèmes infinis hétérogènes, techniques symboliques, abstraction automatique

Commentaires :
Pour une description détaillée de ce sujet, vous pouvez consulter ce document (postscript gzippé) : Sujet-These-Herbreteau-Sutre.ps.gz