Mots-clés | : | Vérification, visualisation, interface graphique, Mec, Tulip, abstraction |
La vérification de modèles permet de vérifier qu'un modèle donné satisfait une propriété donnée. L'automatisation de cette méthode en fait une approche boîte noire qui évite à l'utilisateur de devoir appréhender à quelque moment que ce soit la taille du modèle, qui est souvent énorme.
Cependant, les techniques de visualisation interactive de graphes ont beaucoup progressé ces dernières années et ont donné lieu à des réalisations logicielles performantes, qui permettent de visualiser des graphes de très grande taille. Il devient donc naturel dans la panoplie des outils de vérification de proposer à l'utilisateur de voir le graphe des états accessibles d'un système pour essayer d'obtenir une intuition d'ensemble de son modèle par exemple.
Un intérêt plus important nous semble être la possibilité d'explorer de façon interactive un modèle en déroulant pas à pas les différentes actions possibles du système, en profitant de l'interface graphique offerte naturellement par l'affichage du graphe des états déjà parcourus pour afficher à la demande les informations sémantiques associées à chaque sommet du graphe, et ainsi prendre interactivement et de manière confortable la décision des transitions à suivre pour explorer le modèle. Cette façon d'explorer le graphes des états est aussi appelée simulation : elle simule l'exécution du système, dirigée par l'utilisateur.
Nous souhaiterions que les étudiants réalisent un logiciel couplant le logiciel Mec 5 avec le widget Qt Tulip afin d'offrir à l'utilisateur la possibilité de se balader dans un graphe représenté par sa relation de transition de manière interactive.
Deux points sont importants :
Dans le cadre de l'extension CEGAR de Mec 5 développée par Fares Chucri, il sera sans doute intéressant de considérer l'affichage simultané de deux graphes : un graphe abstrait du modèle, dont chaque sommet est associé à un ensemble de sommets d'un graphe concret. Un troisième point d'étude serait donc de trouver une façon élégante de représenter les relations entre le graphe abstrait et le graphe concret.
Le résultat attendu est la possibilité pour l'utilisateur de lancer le programme réalisé dans le cadre de ce projet en lui passant en paramètre un modèle AltaRica et de pouvoir naviguer dans le modèle avec une interface graphique basée sur Tulip et en utilisant le moteur de calcul de Mec 5. Idéalement, si le temps le permet, une intégration plus fine dans Mec~5 sous la forme d'une commande qui ouvre une nouvelle fenêtre d'exploration serait bien plus adéquate.
Un compilateur C (Mec 5), un compilateur C++ (Qt), le widget Tulip de Qt, et un environnement de développement. Une machine assez performante pour pouvoir tester la réalisation sur des exemples un peu gros.
Nom du responsable | : | Alain Griffault et Fares Chucri |
Adresse | : | LaBRI, bureau 262 |
Téléphone | : | 05 40 00 69 15 |
Fax | : | 05 40 00 66 69 |
Courriel | : | griffaul@labri.fr et chucri@labri.fr |