Description du travail :
AltaRica[1,2] est un langage de modélisation de systèmes développé depuis une
dizaine d'années au LaBRI. Le logiciel ARC[3] permet de
vérifier formellement qu'un système décrit dans le langage AltaRica possède
certaines bonnes propriétés (p.ex. qu'une situation critique ne peut pas se
produire).
Le processus d'étude des comportements d'un système comporte au moins 3
phases:
- La modélisation du système. Les éléments du système et leurs
comportements sont décrits dans un langage formel adapté (p.ex. AltaRica).
Cette description nécessite en général une bonne compréhension du
fonctionnement du système et une forte abstraction, sous certaines hypothèses,
de ces comportements.
- La validation du modèle. Cette étape importante vise à s'assurer que
la modélisation réalisée est correcte du point de vue des hypothèses fixées
et que les comportements du modèle sont une abstraction valide du système réel.
Sans cette étape la vérification effectuée à l'étape suivante n'a pas de sens.
- La vérification des spécifications. Les spécifications du système
sont traduites dans une logique permettant de décrire les comportements[4] puis vérifiées grâce aux algoritmes mis en oeuvre dans ARC.
Dans ce projet nous nous intéressons aux étapes 2 et 3. Nous souhaitons
améliorer la qualité de ces étapes en donnant à l'utilisateur une vision
graphique de son travail. Afin d'atteindre cet objectif l'utilisateur de l'outil
ARC devrait pouvoir:
- simuler les comportements du système/modèle étudié dans une interface
graphique;
- visualiser de manière graphique (sous différentes formes) les composantes
du modèle ainsi que leurs propriétés.
Travail à réaliser :
Le travail à réaliser comporte deux parties:
- Extension du simulateur existant:
ARC possède un embryon de simulateur qui permet de jouer les comportements du
modèle pas à pas. Ce simulateur (réalisé en GTK+) permet:
- de visualiser la valeur des variables du système de manière plus ou
moins ergonomique;
- de simuler un évenement/une action du système et de voir la nouvelle
valeur des variables;
- de recommencer ou de revenir en arrière dans le simulation.
L'objectif ici est d'adjoindre au simulateur une visualisation graphique du
graphe d'état parcouru. L'utilisateur devra pouvoir configurer les informations
représentées sur le graphe (p.ex. variables affichées) et il pourra aussi
utiliser les sommets du graphe pour fixer l'état courant de la simulation (au
lieu d'une simple pile undo).
- Navigateur pour les modèles AltaRica:
Pour les modèles possédant plus d'une dizaine de composants il est avantageux
d'utiliser un navigateur permettant de sélectionner un composant du
système et d'afficher une/des vue/s de ce composant; une vue pourrait
être par exemple la simulation du composant.
Le langage AltaRica est hiérarchique, donc une navigation sous forme d'arbre
est tout à fait adaptée.
Cette tâche devra comportée une sérieuse phase de conception afin de faciliter
l'ajout de nouvelles vues.
Une première vue à réaliser sera une représentation simplifiée sous forme de
boîtes et de fils d'un composant.