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.
Tavail à 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.