VERDON : VERification et test de systèmes réactifs critiques comportant des DONnées
Version 1.31 - Date 2015/09/18 16:11:21
Plan
VERDON is a joint research action supported and funded by the Scientific Department of INRIA.
This action is planned for two years (1998-1999) and involves four research teams at INRIA Rennes/IRISA, INRIA Rhône-Alpes, INRIA Sophia-Antipolis, and LSR-IMAG.
It targets at basic research in the verification and testing of reactive systems (either synchronous or asynchronous) with complex control and data parts, especially by combining model-checking methods with appropriate techniques for data representation and analysis.
Keywords
Abstraction, asynchronous language, concurrency, data flow analysis, data type, distributed system, formal method, model-checking, protocol engineering, reachability analysis, reactive system, state explosion problem, symbolic model-checking, synchronous language, test generation, validation, verification.
VERDON est l'une des "Actions de Recherche Coopérative" (aussi appelées "Actions Incitatives") de la Direction Scientifique de l'INRIA.
Prévue pour une durée de deux ans (1998-1999), cette action regroupe quatre équipes de l'INRIA Rennes, de l'INRIA Rhône-Alpes, de l'INRIA Sophia-Antipolis et du laboratoire LSR-IMAG.
Elle est consacrée à une recherche fondamentale dans le domaine de la vérification et du test de systèmes réactifs (synchrones ou asynchrones) comportant une partie contrôle et une partie donneées de complexité significative, notamment en combinant les méthodes de model-checking avec des techniques appropriées pour la représentation et l'analyse des données.
Mots-clés
Abstraction, analyse d'accessibilité, analyse du flot des données, concurrence, génération de tests, ingénierie des protocoles, langage asynchrone, langage synchrone, méthode formelle, modèle, problème de l'explosion d'états, système distribué, système réactif, type de donnée, validation, vérification, vérification symbolique.
Cette proposition s'inscrit dans la problématique de la conception de systèmes sûrs par l'utilisation de méthodes formelles : utilisation de techniques de description formelles, complétées par des outils informatiques combinant simulation, prototypage rapide, vérification et génération de tests.
Le domaine d'applications visé est vaste : nous nous intéressons à tout système réactif (matériel, logiciel, télécommunications) faisant intervenir du parallélisme asynchrone ou synchrone.
Les trois équipes INRIA impliquées dans cette proposition ont significativement contribué à cette recherche, aussi bien au niveau des langages (synchrones ou asynchrones) et de leur compilation, qu'à celui des algorithmes de vérification et de génération de tests. Dans tous les cas, nous avons eu le souci de mettre en oeuvre nos concepts en réalisant des outils dont la plupart sont actuellement utilisés en milieu industriel (ESTEREL et FC2TOOLS chez DASSAULT, CAESAR et TGV-LOTOS chez BULL, etc.)
Par ailleurs, l'équipe SCOP du laboratoire LSR-IMAG possède une expérience complémentaire dans le domaine des langages de description de données et des méthodes de preuves associées (types abstraits algébriques, méthode B, etc.)
Pour une large part, les méthodes que nous avons appliquées reposent sur des algorithmes d'énumération d'états (model-checking). Le succès de ces méthodes vient de leur spécialisation à des catégories spécifiques de problèmes. En particulier, elles sont bien adaptées aux systèmes réactifs (synchrones ou asynchrones) possédant des espaces d'états finis. Pour ceux-ci, on dispose en effet de procédures de décision efficaces.
Les systèmes réels allient généralement contrôle et données. Les méthodes que nous utilisons actuellement sont capables de traiter ces deux aspects simultanément.
Néanmoins, la partie données est généralement considérée comme un prolongement de la partie contrôle et traitée de la même manière, par énumération de l'ensemble des configurations accessibles.
Cette approche présente plusieurs limitations.
D'une part, les types de données étant généralement infinis, il est nécessaire de les borner à des sous-ensemble finis, ce qui restreint la généralité des résultats obtenus.
D'autre part, les configurations que peuvent prendre les données sont généralement beaucoup plus nombreuses que les configurations accessibles des états de contrôle ; de ce fait, les données sont souvent la cause principale du phénomène de l'explosion d'états.
En pratique, les méthodes de type "model-checking" se révèlent d'une grande efficacité sur les programmes comportant peu de données et dont l'apparente complexité ne provient que du contrôle et des communications. Pour des programmes utilisant intensivement des structures de données complexes, les résultats peuvent s'avérer décevants, à moins que l'utilisateur ne modifie lui-même sa spécification en vue de faire les "bonnes" abstractions sur les données utilisées.
Cette proposition de coopération entre nos équipes a l'ambition de surmonter ce problème en traitant les données de manière spécifique par rapport au contrôle.
Certes, nous n'envisageons pas de résoudre le problème des données dans toute sa généralité, ce qui est plutôt l'apanage des approches basées sur la preuve d'invariants et le démonstration de théorèmes.
Notre objectif est plutôt d'identifier et de construire un corpus de méthodes algorithmiques pour la représentation et le traitement des données afin de les intégrer dans l'approche "model-checking" existante.
Pour mettre en oeuvre notre objectif, nous souhaitons explorer les directions suivantes, qui permettront d'élargir le champ d'application de nos méthodes de vérification et de génération de tests :
- Représentations symboliques et méthodes de décision associées :
- Il s'agit de trouver et d'exploiter les "bonnes" structures symboliques pour la représentation des données.
Parmi celles-ci figurent des extensions des Binary Decision Diagrams permettant la représentation de types finis avec des opérations de nature arithmétique ; des modèles logiques de type Arithmétique de Presburger ou systèmes de contraintes par inéquations en nombres entiers ou réels ; des représentations ensemblistes du type méthode B.
Parmi les travaux existants, il nous semble important d'identifier et de récupérer les procédures algorithmiques combinables avec les acquis du "model-checking" dans une méthodologie étendue de vérification automatique ou largement automatisée.
- Abstractions basées sur des propriétés de régularité :
- On s'aperçoit que les graphes d'états calculés par les outils de vérification ou de génération de tests sont d'une grande régularité, du fait de l'existence de variables n'ayant pas (ou peu) d'influence sur le contrôle.
Appliquées à ces variables, les méthodes énumératives conduisent souvent à un dépliage inutile des graphes d'états, au sens où des états sont différenciés par la valeur de variables "sans intérêt".
Pour résoudre ce problème, nous souhaitons explorer des approches basées sur la représentation symbolique de graphes présentant des régularités, ainsi que l'emploi de techniques d'analyse statique visant à abstraire (ou même éliminer) certaines variables des structures de données servant à coder les états de la spécification.
- Identification de classes d'états équivalents :
- En examinant les graphes d'états produits automatiquement à partir de descriptions formelles en langage de hauts niveau, on constate la présence d'états "redondants", c'est-à-dire d'états qu'il n'est pas pertinent de distinguer.
Bien souvent, ces états redondants sont dus à la présence de données dans les descriptions. C'est notamment le cas des états qui ne se distinguent que par la valeur de variables "mortes", c'est-à-dire de variables dont la valeur ne sera plus réutilisée par la suite avant d'être réaffectée.
Pour résoudre ce problème, nous souhaitons détecter statiquement des classes d'états "équivalents" au sens des propriétés que l'on doit vérifier ou des objectifs de test que l'on doit atteindre. Ceci peut se faire de plusieurs manières, par exemple par une analyse statique du flot de contrôle et du flot de données dans les programmes parallèles, avec des techniques de calcul de dépendances, des heuristiques de coloriage de graphes, etc.
- Prise en compte des données dans la vérification compositionnelle :
- Une des approches les plus efficaces pour lutter contre l'explosion d'états dans le cadre de l'approche "model-checking" consiste à utiliser des méthodes de vérification compositionnelle, basées sur la décomposition du système à vérifier en sous-systèmes plus simple.
Habituellement, cette décomposition est faite selon les opérateurs de parallélisme du langage. Nous souhaitons étudier les implications de ce découpage sur le flot des données, ainsi que la faisabilité d'autres schémas de décomposition basés sur le flot des données.
- Génération de tests paramétrés :
- En général, les outils de vérification fournissent des diagnostics sous forme de séquences d'exécution dans lesquelles les variables et les communications ont des valeurs instantiées.
Toutefois, on pourrait imaginer des diagnostics de vérification plus généraux dans lesquels les valeurs des variables seraient manipulées symboliquement.
Ceci est nécessaire pour les tests, qui ont souvent vocation à être intégrés dans des documents de normalisation. C'est pourquoi il nous semble important de savoir engendrer des tests comportant des paramètres symboliques et des calculs sur des données, assortis des structures de contrôle usuelles (boucles conditionnelles, etc.)
Ceci requiert la mise en oeuvre des approches mentionnées ci-dessus (représentation symbolique, abstractions, etc.)
A terme, on peut espérer que les solutions dégagées dans le cadre de cette collaboration seront implémentées dans les outils développés par nos équipes (notamment CADP, FC2TOOLS et TGV).
Liste des participants
Didier Bert, Michel Bourdellès, Benoît Caillaud, Hubert Garavel, Thierry Jéron, Mihaela Sighireanu, Robert de Simone.
Programme des exposés
- Didier Bert
Axes de recherche de l'équipe SCOP du laboratoire LSR
Spécification et vérification de systèmes en B
- Hubert Garavel
Axes de recherche de l'équipe VASY
- Robert de Simone
Axes de recherche de l'équipe MEIJE
- Thierry Jéron
TGV: Génération automatique de tests de conformité pour les protocoles
- Benoît Caillaud
Réflexions sur la dérivation de tests symboliques
- Michel Bourdellès
Vérification de processus synchrones comportant des données
- Mihaela Sighireanu
Types de données et modules dans les langages E-LOTOS et LOTOS NT
Liste des participants
Didier Bert, Amar Bouali, Michel Bourdellès, Benoît Caillaud, Hubert Garavel, Thierry Jéron, Radu Mateescu, Marie-Laure Potet, Annie Ressouche, Mihaela Sighireanu, Robert de Simone.
Programme des exposés
- Didier Bert et Marie Laure Potet
Etude de cas d'un système de contrôle d'accès à des bâtiments
(pour en savoir plus...)
- Hubert Garavel
Modélisation d'un système d'entrées-sorties SCSI-2
- Leslie Lamport
The Bakery Algorithm Rises Again, or Golden Oldies from the '70s
- Radu Mateescu
Vérification de propriétés temporelles comportant des données
- Mihaela Sighireanu
Spécification du contrôle dans les langages E-LOTOS et LOTOS NT
- Thierry Jéron
Génération de tests symboliques
Liste des participants
Didier Bert, Claude Chaudet, Hubert Garavel, Claude Jard, Thiery Jéron, Aldo Mazzilli, Marie-Laure Potet, Eric Rutten, Massimo Zendri.
Programme des exposés
- Radu Mateescu
Vérification en XTL du système SCSI-2
(PDF ou PostScript)
- Thierry Jéron
Génération de tests symboliques
- Didier Bert
Etude B du système d'entrées-sorties SCSI-2
(PDF ou PostScript)
- Claude Chaudet
Spécification en LOTOS NT du système SCSI-2
Liste des participants
Didier Bert, Claude Jard, Thierry Jéron, Radu Mateescu, Brian Nielsen, Annie Ressouche, Vlad Rusu, Jean-Marc Sanquer.
Programme des exposés
- Vlad Rusu
Symbolic Test Generation and Abstraction
Black-box testing is an approach that aims at detecting bugs in real
protocol implementations. Recently there has been progress in the
direction of automating the test-generation process, with
industrial-strength tools coming up. These tools deal with the data
part of a specification in a purely enumerative manner. In this talk I
will present some background and describe ongoing work on how to
generate symbolic tests from symbolic specifications. A symbolic test
case is a parametrized scenario in which the verdict on the
implementation (pass, fail) depends on relations between the symbolic
inputs and outputs. The approach allows to find domains of input
values that should be tested to have a good coverage. This results
in a methodology to generate symbolic test cases, in which abstraction
is used to simplify detailed specifications from irrelevant details.
An example of applying the methodology to a portion of the SSCOP
protocol will be presented.
- Jean-Marc Sanquer
Vérification et correction de tests symboliques
- Brian Nielsen (Aalborg University, Denmark)
Automatic Test Derivation for Real-Time Systems
For real-time systems the timeliness of a response is as important as
the correct type of response. An actual implementation of such a system
must therefore be checked by means of testing with respect to both
logical and timing errors.
We propose an algorithm for automatically deriving test-cases from
specifications given as Event Recording Automata, a determinizable
subclass of timed automata. To aid test selection we partition the state
space of the specification into coarse equivalence classes and cover
each with at least one test. The reachable parts of the equivalent
classes can be computed by using symbolic techniques developed in the
field of verification of real-time systems.
Our technique is implemented in a prototype tool which uses difference
bound matrixes as the underlying data-structure.
- Radu Mateescu
Automatic Diagnostic Generation for "on the fly" Model-Checking
An efficient technique for on-the-fly model-checking uses resolution
of Boolean Equation Systems (BESs). The verification problem, expressed
either as a bisimulation between two Labelled Transition Systems (LTSs),
or as a temporal logic formula over an LTS, is reduced to the local
resolution of a BES, i.e. the calculus of the value of a particular
variable of the BES. An important efficiency criterion for this class
of algorithms is their average complexity, which should be kept as small
as possible in order to avoid the construction of a "too large" part of
the LTS during the verification.
We present a new algorithm to perform the local resolution of a BES
which appears to have a better average complexity than currently available
algorithms. Moreover, the algorithm allows to generate diagnostics, i.e.
"relevant" portions of the LTS that explain the truth value of the formulas
being checked.
The algorithm has been used as basis for constructing a linear-time
on-the-fly model-checker for regular alternation-free mu-calculus.
The tool, called EVALUATOR version 3.0, has been implemented on top
of the Open/Caesar environment of CADP and experimented on various
examples.
- Annie Ressouche
Compilation d'Esterel en Verilog-VHDL
Liste des participants
Didier Bert, Moëz Cherif, Hubert Garavel, Jean-Claude Fernandez, Claude Jard, Thierry Jéron, Radu Mateescu, Marie-Laure Potet, Vlad Rusu, Irina Smarandache.
Programme des exposés
- Vlad Rusu
An Approach to Symbolic Test Generation
(common work with Lydie du Bousquet and Thierry Jéron)
Protocol specifications are often represented as transition systems
extended with variables such as booleans, counters, and arrays. It
is a common practice to use the formal specifications in order to
produce functional test cases, which are themselves extended transition
systems. Quite evidently, the process is error-prone if the "test writer"
is not assisted by formal tools. We propose an approach to generate
correct-by-construction test cases from symbolic specifications. The
approach uses static analysis and the PVS theorem prover, and is automated
in a significant proportion. We demonstrate the approach on a simple
example: the sender of the BRP protocol.
- Radu Mateescu
Résolution "à la volée" des systèmes d'équations booléennes paramétrées
Les techniques de vérification basées sur les modèles
(model-checking) permettent de décider si un système fini
satisfait une certaine propriété, exprimée au moyen d'un
automate ou d'une formule de logique temporelle. Pour vérifier
des systèmes réalistes, en pratique il est nécessaire de
pouvoir exprimer et vérifier les propriétés en tenant compte
des données manipulées dans le système. Une technique de
vérification simple et efficace consiste à traduire le problème
vers un système d'équations booléennes paramétrées (SEBP), qui
est résolu de manière locale (c.a.d. on calcule la valeur d'une
seule variable booléenne, en fixant la valeur de ses paramètres).
Nous présentons un algorithme de résolution qui fonctionne par
expansion ``en avant'' de l'instance de la variable à calculer et
par propagation ``en arrière'' des instances évaluées à vrai.
Cet algorithme généralise l'approche classique ``à la volée''
pour les SEBs sans paramètres et permet en outre de générer des
diagnostics (exemples et contre-exemples) pour la variable d'intérêt.
Nous illustrons l'application de cette technique au cas d'une logique
temporelle étendue avec des données et nous discutons les applications
potentielles pour la génération de tests paramétrés.
- Didier Bert
Liaison B - CADP
- Hubert Garavel
Optimisation des types structurés dans le compilateur Caesar.adt
(travail en commun avec Radu Mateescu)
Après une étude comparative des différents paradigmes utilisés dans les langages impératifs, fonctionnels, algébriques et à objets pour la représentation des types structurés (listes, ensembles, arbres, etc.), nous présentons les principes du compilateur Caesar.adt et les récentes optimisations mises en oeuvre dans ce compilateur pour minimiser le coût en mémoire de l'implémentation des types structurés. Sur l'exemple SCSI-2 étudié dans l'action Verdon, ces optimisations ont permis un gain de mémoire significatif (7 Moctets au lieu de 955 Moctets).
Ajouté le 18 juin 2003 :
L'action de recherche coopérative VERDON s'est effectuée sur une durée de 2 ans, du 1er janvier 1998 au 31 décembre 1999. Les projets MEIJE, PAMPA et l'action VASY-RA de l'INRIA, ainsi que l'équipe SCOP du laboratoire LSR-IMAG ont participé à cette action.
D'un montant de 120 kF, le budget de VERDON a été employé à effectuer des missions (réunions régulières, de 2 à 3 fois par an), des visites, ainsi qu'à payer des stagiaires :
- Francis Cave (équipe SCOP, juillet-septembre 1999) : connexion de B aux systèmes de transitions
- Claude Chaudet (action VASY-RA, février-juin 1999) : compilation des types de données LOTOS, E-LOTOS et LOTOS NT
- Adrian Curic (projet VASY, en 2000, sur le reliquat de budget de VERDON) : factorisation de termes algébriques pour la vérification énumérative
- Jean-Marc Sanquer (projet PAMPA, août-septembre 1999) : vérification de tests symboliques.
Pour l'action VERDON, une étude de cas commune a été choisie : une version du protocole SCSI-2 fournie par Massimo Zendri (Bull), dans laquelle on peut mettre en évidence une erreur (famine) pour une certaine configuration des valeurs du système. Cette étude cas a été modélisée dans divers langages/formalismes (B, LOTOS, LOTOS NT et SDL) afin de permettre la comparaison des approches. Ce travail a ensuite servi de support à des démonstrations effectuées dans le cadre de la journée technologique DYADE le 21 janvier 2000.
La participation de l'équipe SCOP à l'action VERDON a permis d'approfondir les rapprochements qui existent entre la technologie B et les langages basés sur le modèle des systèmes de transitions étiquetées : langages à commandes gardées, algèbres de processus (LOTOS), etc.
Le travail de SCOP a porté sur l'étude du formalisme et de la méthode B pour spécifier des systèmes à données complexes. Il s'agit de calculer des systèmes de transitions finis à partir de descriptions B et d'effectuer des raffinements sur les automates construits.
L'étude de cas SCSI-2 a été spécifiée et raffinée, et les propriétés de non-famine du protocole SCSI-2 ont été formalisées. Enfin, l'étude de la connexion entre l'atelier B et la boîte à outils CADP a été entreprise : ce travail se poursuit actuellement dans le cadre du stage de DEA de Francis Cave. Un article sur la construction de systèmes de transitions finis à partir de systèmes abstraits B est soumis à publication.
La participation de MEIJE a été centrée d'une part sur l'interconnexion entre CADP et les outils de vérification Fc2Tools (développés par MEIJE) basés sur les automates et, d'autre part, sur la vérification de programmes comportant des données (thèse de Michel Bourdellès). Après sa thèse, Michel Bourdellès a effectué un stage post-doctoral dans le projet PAMPA.
Pour PAMPA, l'action VERDON a constitué le forum pour démarrer un nouvel axe de recherche sur la génération de tests symboliques. Il s'agit, à partir d'une spécification paramétrée et manipulant des données et d'un objectif de test du même type, de produire un programme de test du même type.
L'idee sous-jacente est la combinaison de techniques de preuve avec les algorithmes de parcours de graphes existant dans l'outil TGV. Ceci nécessite de définir un produit de systèmes de transitions symboliques. Dans un premier temps, PAMPA a travaillé sur le problème, plus simple, de la vérification de tests symboliques : il s'agit de définir des critères exprimant qu'un test est correct à la fois par rapport à la spécification et à l'objectif de test (par exemple, qu'il ne peut pas rejeter une implémentation conforme à la spécification). Ensuite, PAMPA a cherché à générer des tests corrects par construction, pour les critères de correction sus-mentionnés.
Les contributions de VASY ont porté sur deux axes : d'une part, l'évaluation de formules de logique temporelle comportant des variables typées et la génération de diagnostics, et d'autre part, les techniques de compilation et de vérification pour le langage LOTOS NT (une variante simplifiée de la future norme E-LOTOS). Ces travaux menés dans le cadre de VERDON ont donné lieu à des publications et à des logiciels diffusés : le vérificateur EVALUATOR 3.0 (intégré dans les dernières versions de CADP) et le compilateur TRAIAN 2.0.
L'action VERDON a renforcé les liens qui existaient déjà entre PAMPA et VASY, notamment dans le cadre de collaboration avec BULL (intégration de TGV dans CADP) et ALCATEL (connexion à CADP des outils UML de PAMPA). A plus long terme, certains thèmes abordés dans VERDON suggèrent de futures pistes de collaboration :
- les algorithmes d'évaluation pour les logiques temporelles et de génération de diagnostics pourraient aussi servir à produire des tests définis par des objectifs de tests "symboliques" ;
- le modèle des IOSTS (Input/Output Symbolic Transition Systems) utilisé pour la génération de tests symboliques est très proche du modèle "réseau de Pétri étendu" produit par le compilateur CAESAR à partir de programmes LOTOS séquentiels ;
- les techniques de compilation et de vérification (factorisation de termes) développées pour LOTOS et LOTOS NT pourraient être aussi appliquées à UML (outil UMLAUT de PAMPA).
En résumé, l'action VERDON a été le lieu d'une "fertilisation croisée" entre les équipes travaillant dans des domaines connexes :
- en renforçant les collaborations existantes (visites, échanges d'étudiants),
- en ayant une meilleure compréhension des travaux réciproques des partenaires (notamment des rapports entre les problématiques de la vérification, de la preuve et du test),
- en donnant à de jeunes chercheurs l'occasion de présenter leurs travaux.
Enfin, l'action VERDON a trouvé un prolongement industriel avec le démarrage de l'action FormalCard lancée par le Comité de Pilotage du GIE Bull/INRIA "Dyade" le 27 avril 2000 : d'une durée de 2 ans, l'action FormalCard vise à appliquer les technologies du test symbolique (PAMPA) et de la compilation de LOTOS NT (VASY) aux cartes à puces développées par Bull CP8.
Back to the VASY Home Page
