|
|
|
|
| Projets INRIA | PAMPA (Rennes)
VASY (Grenoble) |
| Personnels INRIA | Hubert Garavel (Chargé de Recherche)
Thierry Jéron (Chargé de Recherche) Vlad Rusu (Chargé de Recherche) |
| Ingénieurs Experts | Dunkan Clarke (à partir du 1er septembre 2000)
Frédéric Lang (à partir du 25 juillet 2000) |
| Chercheur Doctorant | Elena Zinovieva, bourse Inria |
| Personnels Bull | Sébastien Gelgon (jusqu'en juin 2000)
Nicolas Lasselin (de juillet 2000 à octobre 2000) Jean-Michel Ravon (à partir de novembre 2000) Massimo Zendri (jusqu'au 31 mars 2000) |
La certification par des méthodes formelles répond à une demande croissante dans l'industrie, en raison de l'apparition de nouvelles normes ("Critères Communs") qui préconisent, à partir d'un certain niveau de sécurité, l'utilisation de telles méthodes. L'objectif principal de l'action FormalCard est de réaliser un environnement de validation formelle de logiciels embarqués sur cartes à puces par vérification automatique et génération de tests, en vue de permettre leur certification. Notre deuxième objectif est de démontrer l'applicabilité de techniques symboliques de génération de tests sur des cas d'étude de taille industrielle.
L'action est orientée principalement vers la validation de logiciels embarqués sur cartes à puces. Les retombées scientifiques devraient permettre d'appliquer les techniques et outils à d'autres domaines d'application tels que les protocoles de communication.
Pour la vérification par exploration de l'espace d'états nous utilisons la boîte à outils CADP, développée notamment par l'équipe VASY à l'Inria Rhône-Alpes. Pour la génération de tests par des méthodes énumératives, nous utilisons l'outil TGV, développé par l'équipe PAMPA à l'Inria Rennes. Pour la partie plus exploratoire sur l'utilisation de méthodes symboliques, nous utilisons le langage IF du laboratoire Verimag, ainsi que le prouveur PVS et les procédures de décision ICS du Stanford Research Institute.
L'action FormalCard comporte trois sous-projets :
L'objectif est de donner une description formelle (syntaxe, sémantique statique et dynamique) du langage qui sera utilisé pour décrire les applications à valider. Ce langage doit satisfaire plusieurs critères :
Nous basons la conception de ce langage sur les travaux de normalisation effectués au sein de l'ISO de 1992 à 2000 pour la définition du langage E-LOTOS. Un sous-ensemble du langage LOTOS NT, développé par l'équipe VASY, satisfaisant les besoins des ingénieurs de Bull et permettant de décrire un automate (séquentiel) à entrée/sortie et à commandes gardées sera sélectionné. Une expérience réussie de spécification (mini-système d'exploitation pour carte) a déjà été menée en 1999 avec ce type de langage.
En 2000, nous avons utilisé intensivement le langage LOTOS NT, en particulier pour la construction de deux compilateurs destinés à être intégrés à la boîte à outils CADP :
Ce travail nous a permis d'expérimenter en vraie grandeur la technologie de construction de compilateurs basée sur la partie données du langage LOTOS NT qui sera utilisée pendant la suite de l'action FormalCard afin de construire le compilateur pour la partie contrôle de LOTOS NT.
Il s'agit de spécialiser au domaine de la carte à puce certaines techniques bien établies pour lesquelles nous disposons d'outils efficaces (CADP pour la vérification, TGV pour la génération de tests).
Un compilateur pour le langage de description formelle défini dans le sous-projet précédent sera réalisé. Ce compilateur génèrera du code C compatible avec l'interface Open/Caesar. Ceci permettra :
En 2000, nous avons poursuivi nos travaux relatifs au développement du compilateur TRAIAN pour le langage LOTOS NT, dont la version 1.0 avait été distribuée en septembre 1998 (thèse de Mihaela Sighireanu).
En février 2000, une nouvelle version 2.0 de TRAIAN a été produite, qui comporte de nombreuses améliorations et corrections de bogues (environ 45). Cette version introduit de nouvelles fonctionnalités, notamment la génération de code C pour la partie données de LOTOS NT et le portage vers de nouvelles architectures (SunOS, Solaris, Linux et Windows).
En novembre 2000, une nouvelle version 2.1 de TRAIAN a été produite, qui comporte quelques corrections de bogues, ainsi qu'une nouvelle édition du manuel de référence du langage LOTOS NT entièrement relue et corrigée.
Les techniques énumératives de génération de tests ont des limites inhérentes, dues à l'explosion combinatoire. De plus, les cas de test produits sont complètement instanciés, contrairement à la pratique industrielle (cf. le langage TTCN - norme ISO 9646), qui veut que les cas de test soient de "vrais" programmes avec variables et paramètres.
Nous proposons d'explorer la démarche complémentaire, qui est de produire des cas de test symboliques afin de combattre le problème d'explosion combinatoire et d'obtenir des cas de test conformes à la pratique industrielle. Cette démarche repose sur la possibilité de découvrir et d'utiliser, dans la spécification du système en cours de test, des relations entre le contrôle et les données. Ces relations (ou invariants) sont recherchés automatiquement en utilisant des techniques d'analyse statique. De tels cas de tests abstraits permettent l'instanciation "intelligente" afin de couvrir différents scénarios d'interactions.
En 2000, les fondements théoriques de ce travail ont été publiés dans l'article An approach to symbolic test generation. L'implantation des opérations nécessaires pour la génération de tests symboliques est en cours. Nous avons également étudié des techniques de simulation symbolique pour la couverture structurelle des cas de tests (article soumis) et l'implantation de ce travail est également en cours.
Back to the VASY Home Page