Next: Sujet : Modélisation et
Up: Sujets de thèse autour
Previous: Le thème scientifique
Le modèle AltaRica est un modèle basé sur les automates à
contrainte. C'est une extension du modèle des systèmes de transition
et de synchronisation étudié depuis longtemps dans l'équipe MVTsi.
Dans le modèle AltaRica, une transition n'est pas simplement :
``NomEtat'' |- ``EtiquetteTransition -> ``NomEtat''
mais plus généralement
``ContrainteSurVariables'' |- ``Evénement -> ``AffectationVariables'' priorité ``Entier''
Ce modèle à été choisi pour diverses raisons :
- sa simplicité,
- son pouvoir d'expression : il contient tous les modèles utilisés en
vérification, test et sûreté de fonctionnement,
- sa proximité du modèle Arnold-Nivat.
Le langage AltaRica doit permettre de décrire un système complexe en
terme d'un automate à contrainte. Pour cela divers concepts sont
introduits afin de faciliter la tâche de l'utilisateur.
- La hiérarchie
- un automate à contrainte peut-être décrit comme
un arbre d'automates à contrainte. Cela permet un découpage
fonctionnel, et facilite grandement la compréhension du système.
- Variables d'états/variables de flux
- Les premières permettent de
décrire les comportements des sous-systèmes (les noeuds de l'arbre des
automates), les secondes les échanges de données entre eux (les arcs
de l'arbre). Plus important, la sémantique de l'évolution d'un système
en fonction du temps n'est pas la même pour ces deux types de données.
- La synchronisation
- les événements sont par défauts
indépendants, c'est à dire que leurs occurrences sont asynchrones, mais
il est possible de contraindre plusieurs événements afin qu'ils soient
simultanés.
En fait, il existe deux langages AltaRica, l'un textuel et l'autre
graphique, mais totalement équivalent.
Le langage de description AltaRica se veut fédérateur pour un ensemble
de problèmes liés à l'étude des systèmes critiques et/ou
complexes. Cela sous-entend que l'on puisse à partir d'une description
AltaRica d'un système :
- calculer son arbre de défaillances, afin d'en extraire les
coupes minimales et autres résultats qui interresseront le fiabiliste;
- calculer des scénarios aboutissant soit à un événement redouté,
soit à une situation particulière, afin de pouvoir tester si le
système réel réagit conformément à ses spécifications.
- montrer que des propriétés de fonctionnement souhaitées sont
bien réalisées.
- ...
Deux possibilités : un outil unique ayant l'ensemble des
fonctionnalités, ou bien, un outil dédié à la saisie du modèle, et des
compilateurs vers des outils spécialisés. Pour de nombreuses raisons,
seul le second choix est raisonnable. Le projet AltaRica s'appuie donc
sur un ensemble (non limité) d'outils, en fait représentatif de
modèles mathématiques dérivables à partir des automates à contraintes.
- Modèle Booléen
- Aralia, outil de calcul sur les arbres de défaillances.
- Réseau de Petri
- Arabica, outil de calcul sur les réseaux de
Petri stochastiques.
- Automates à contraintes
- Toupie, calcul sur les domaines
finis.
- Système de transition
- Mec, vérificateur de modèles.
- ...
Le projet AltaRica, piloté par le LaBRI, est financé en partie par
des industriels et par la région Aquitaine. De ce fait les objectifs
de différentes natures sont définis régulièrement par les membres du
club AltaRica. La phase 2 (l'actuelle) du projet comporte :
- du cours terme
- Cela regroupe principalement des tâches de
développement pour lesquelles les travaux de recherches ont déjà été effectués.
- une consolidation du langage de description AltaRica.
- le compilateur d'un arbre d'automates en un automate.
- le compilateur d'un automate vers les arbres de défaillances.
- le compilateur d'un automate vers les réseaux de Petri.
- l'interface de saisie d'une description AltaRica.
- la simulation d'une description AltaRica.
- du moyen terme
- Cela regroupe principalement des travaux de
recherches sur lesquels il est nécessaire de travailler maintenant, afin
d'aboutir soit à la faisabilité, soit au rejet.
mais également :
- du long terme
- Cela regroupe uniquement des travaux de
recherches qui pourrait influencer les phases ultérieures du projet.
- les preuves formelles afin de pouvoir traiter des systèmes plus importants.
- l'interprétation abstraite afin de diminuer la taille du
problème par une simple analyse de la description.
Next: Sujet : Modélisation et
Up: Sujets de thèse autour
Previous: Le thème scientifique
Equipe Modélisation, Vérification et Test des systèmes informatisés
Fri May 15 10:32:44 CEST 1998