Sujet : Construction automatique de systèmes abstraits au moyen des prédicats.



Responsable : K. Musumbu
Téléphone : 05 40 00 38 76

e-mail : musumbu@labri.fr

Présentation du sujet : Dans le cadre du model-checking, l'abstration est la technique la plus importante pour réduire le problème de l'explosion combinatoire du nombre d'états de systèmes. Elle consiste à trouver une application surjective entre le domaine réel de valeurs de variable avec un domaine abstrait, plus réduit. En prolongeant cette application aux états et transitions du système, il est possible d'obtenir un système abstrait plus réduit qui simule le système original. Grâce à sa taille réduite, il est facile d'appliquer les algorithmes de model-checking et de vérifier les propriétés désirées du modèle réel sur le système abstrait.

Travail à faire : Il s'agit d'implémenter un algorithme de construction des abstractions utilisant les prédicats du système comme des variables. Un sous-ensemble quelconque du système abstrait peut-être représenté par une expression booléenne sur les prédicats( ici considérés comme variables). La définition d'un programme abstrait est très précise et nécessite la validation d'un nombre important d'assertions. Pour réduire, ce nombre on peut calculer une abstraction moins précise. Pour cela, on ne considérera pas toutes les expressions booléennes mais uniquement le sous-ensemble des monômes de longueur k.

Mot-clés : Model-checking, automate, synchronisation, abstraction.

Références : notes du cours et voir sur internet

Commentaires éventuels : Ce sujet est fortement recommandé aux étudiants qui ont suivi l'UE Technologie de la Vérification, qui constitue le pré-requis nécessaire.