Projet AGATHA
Contexte
Les méthodes formelles ont entraîné le développement de techniques
d'analyse de systèmes et de génération automatique de tests à partir de leurs
spécifications. Cela permet d'avoir une évaluation des comportements
possibles d'un système au plus tôt. L'impact économique de cette étape
d'analyse de spécification est considérable, car elle réduit à la fois les
temps et les coûts de validation, alors qu'elle augmente la fiabilité du
système. Mais ces techniques formelles sont généralement assez complexes, ce
qui explique qu'à ce jour, leur usage dans l'industrie soit encore
faible.Pour ces raisons, il est fondamental de fournir des outils
automatiques qui mettent en oeuvre ces technologies, sans demander à
l'utilisateur potentiel de compétences supplémentaires.
Généralités
La méthode et l'outil AGATHA développés au CEA LIST sont dédiés à
la validation et à la génération automatique de tests. Basés sur l'exécution
symbolique de systèmes constitués d'automates concurrents, AGATHA permet de
générer un arbre d'exécution exhaustif qui couvrent l'ensemble des
comportements du système analysé, et fournit pour chaque comportement
identifié un test numérique. Entièrement automatique, AGATHA peut être
utilisé comme une boîte noire dans un environnement d'outils industriels tels ObjectGeode, StateMate
ou Objecteering. Avec AGATHA,
les utilisateurs peuvent générer des scénarios et les exécuter dans le
simulateur de leur environnement. AGATHA est conçu pour prendre en compte le
système évalué tout entier ou une partie du système, ce qui permet de faire
des validation intermédiaires au cours de son élaboration.
La figure suivante montre la fenêtre principale de l'outil AGATHA :
Principes de l'outil AGATHA
L'outil AGATHA génère un graphe d'exécution symbolique, qui décrit tous
les comportements du système. La figure suivante montre l'architecture de
l'outil AGATHA :
Plusieurs techniques formelles sont utilisées pour le calcul :
L'exécution symbolique : Le problème majeur des techniques
numériques est l'explosion combinatoire due au domaines de variations
des paramètres du système. Ces domaines peuvent être très grands, ou
même infinis. Le calcul symbolique permet de prendre en compte de tels
domaines parce qu'il exécute tous les comportements qui ne sont pas
équivalents, mais sans effectuer de calculs redondants lorsque des
valeurs différentes des variables correspondent au même comportement
(i.e. au même chemin d'exécution). Les paramètres d'entrées ne sont pas
évalués numériquement mais apparaissent sous forme de constantes
symbolique dans les gardes des transitions qui sont exécutées. Les
gardes des transitions exécutées dans un chemin d'exécution sont
intégrées dans une contrainte qui est la condition de chemin, et qui
doit être satisfaite pour que le chemin en question soit exécuté : cette
condition de chemin n'est autre que la conjonction logique des gardes
des transitions du chemin ; la résolution de cette condition de chemin
donne une séquence de valeurs numériques d'entrées du système qui permet
de réaliser un test concret (par exemple dans un simulateur classique).
Procédures de réduction : Le point délicat de l'exécution
symbolique est la réduction des expressions qui sont générées dans la
condition de chemin. Les expressions symboliques peuvent devenir
considérables, c'est pourquoi il est nécessaires de les simplifier à la
volée, afin que les temps de calculs intermédiaires ne deviennent
prohibitifs. Ces simplifications sont faites par réécriture grâce à
l'outil CafeObj. L'outil de calcul polyhédrique Omega est également
utilisé pour évaluer des inclusions de domaines sur les variables, ce
qui permet également de réduire l'arbre d'exécution et de le ramener à
un arbre fini.
Composition : Le processus d'exécution symbolique est
appliqué sur un automate du système, mais en général le système est
constitué de plusieurs automates, qui doivent donc être fusionnés. La
méthode de fusion est la composition introduite par Milner. L'automate
global équivalent à l'ensemble est constitué des transitions de chaque
automate élémentaire, et les transitions qui sont en rendez-vous sont
synchronisées et remplacées par des transitions équivalentes où l'on a
éliminé les paramètres de communications.
Solveur de contrainte : Lorsque l'arbre d'exécution a été
construit, tous les comportements du système sont accessibles par
consultation de cet arbre. Les livelocks et les deadlocks sont visibles.
Un solveur de contraintes, l'outil Omega qui est un outil de calcul dans
l'arithmétique de Presburger, peut être utilisé pour obtenir les valeurs
numériques des paramètres du système par résolution des contraintes de
chemin. Chaque condition de chemin donne une séquence d'entrée du
système (par défaut, on calcule une solution par contrainte, considérant
que d'autres solutions numériques sont redondantes du point de vue de
l'identification des comportements du système).
La figure suivante montre les détails de l'architecture du noyau
d'AGATHA:
Applications d'AGATHA
MUTATION le projet implique le CEA-LIST, TAS (THALES Airborne System), TRT (THALES Research and
Technology) et l'INRIA. Ce projet appartient au programme
CARROLL. Le but de ce
projet est d'accroître la productivité de la phase de validation du
processus de développement. Dans ce contexte, nous utilisons AGATHA pour
générer automatiquement des tests sur des modèles UML de TAS.
EDEN est un projet RNTL (Réseau National des Technologies Logicielles)
projet qui a commencé en 2003. Le projet EDEN implique les partenaires
suivants : SCHLUMBERGER (SEMA - CP8), TRUSTED-LOGIC, VERIMAG, CEA-CESTI, CEA-LIST.
L'objectif du projet est d'offrir un environnement capable de faciliter
le développement et la validation de systèmes embarqués en respectant
les exigences des critères communs (domaine des cartes à puces) au
niveau formel. Dans ce contexte, AGATHA est utilisé pour générer des
tests de conformité entre ces niveaux.
STACS est
un projet qui implique CEA LIST, LaMI (Laboratoire
de Méthodes Informatiques
de l'Université d'Evry) THALES
Communication
et Ligeron SA. C'est un projet qui est
soutenu par le
RNRT (Réseaux National
de Recherche en Télécommunication). L'objectif est de trouver une méthode de
validation
compositionnelle pour les systèmes de télécommunication en utilisant les
techniques de test. Ces systèmes sont hétérogènes dans le sens où ils sont basés
sur des modèles d'automates concurrents dans des formalismes différents tels
SDL, UML ou Esterel.
AGATHA permet la génération de tests pour la validation de
fonctionnalités de systèmes temps-réels construits à partir de la
méthodologie Accord/UML .
AIT-WOODDES
Equipe AGATHA
Publications
de l'équipe AGATHA
|
