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


Executive Summary

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.


Résumé

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.


Participants


Contexte scientifique

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.


Programme de recherche

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).


Réunion de travail du 11 février 1998 (Ecole des Mines, Paris)

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


Réunion de travail du 15 septembre 1998 (INRIA Sophia-Antipolis)

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


Réunion de travail du 3 mars 1999 (INRIA Rhône-Alpes)

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


Réunion de travail du 3 juin 1999 (INRIA Rennes)

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


Réunion de travail du 16 décembre 1999 (LSR-IMAG, Grenoble)

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


Etude de cas commune (bus SCSI-2)

Ajouté le 18 juin 2003 :

Bilan de l'action de recherche coopérative VERDON

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 :

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.

En résumé, l'action VERDON a été le lieu d'une "fertilisation croisée" entre les équipes travaillant dans des domaines connexes :

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