Séminaire VASY 2003
Saint Pierre de Chartreuse (Isère)

Mardi 10 Juin 2003

9h30

Ouverture

9h30 – 11h00

Wendelin Serwe

Abstraction de piles d'appel pour la vérification interprocédurale de programmes impératifs

Nous nous intéressons à la vérification de programmes impératifs avec procédures récursives.  Nous présentons une application de la technique de l'interprétation abstraite afin de relier la sémantique classique de programmes impératifs à une sémantique abstraite par une connexion de Galois.  Dans un deuxième temps, nous utilisons des techniques intra-procédurales pour obtenir une représentation calculable. Notre approche permet ainsi la réutilisation de techniques existantes et ajoute une flexibilité supplémentaire, car elle permet de garder une partie importante de l'information contenue dans la pile d'appel du programme analysé.

11h30 – 12h30

Hubert Garavel

DISTRIBUTOR : un outil pour le model-checking massivement parallèle

La vérification énumérative des systèmes distribués à nombre fini d'états nécessite souvent la génération (d'une large partie) de l'espace d'états du système à vérifier. A cause du problème de l'explosion d'états, cette opération peut être coûteuse en mémoire et en temps de calcul. Les techniques de parallélisation sont susceptibles  d'optimiser les performances de la construction des espaces d'états.  Nous présentons des algorithmes parallèles pour construire les espaces d'états (ou les systèmes de transitions étiquetées) sur un réseau ou une grappe de stations de travail. Chaque noeud du réseau construit une partie de l'espace d'états, toutes les parties étant rassemblées pour former l'espace d'états complet après terminaison du calcul parallèle. Ces algorithmes ont été implémentés dans la boîte à outils CADP et expérimentés sur différentes applications distribuées spécifiées en LOTOS. Les résultats obtenus mettent en évidence des gains en vitesse linéaires et un bon équilibrage de charge entre les noeuds du réseau.

Déjeuner

15h30 – 16h15

Nicolas Descoubes

La bibliothèque Caesar_Network pour le model checking distribué

Dans le domaine de la vérification, les limites physiques des machines sont souvent atteintes, restreignant ainsi la taille des problèmes traitables. Une solution consiste à distribuer les algorithmes pour les faire tourner sur plusieurs machines, multipliant ainsi la puissance de calcul et la capacité mémoire. Lors de l'implémentation de tels algorithmes revient systématiquement le problème du mode de communication entre les différents noeuds. La bibliothèque Caesar_Network propose un ensemble de primitives de configuration de réseau et d'échanges de messages facilitant l'implémentation de ces algorithmes distribués. L'objectif de l'exposé est alors de présenter les fonctionnalités et le fonctionnement de cette bibliothèque, le tout accompagné d'exemples de mise en oeuvre.

16h15 – 17h30

Hubert Garavel

Caesar.adt : un compilateur efficace pour les types abstraits LOTOS

Nous présentons le compilateur CAESAR.ADT dont le rôle est de traduire en langage C les définitions de types abstraits algébriques contenues dans les descriptions LOTOS. Grâce à ce compilateur, il est possible d'exécuter la partie données des descriptions LOTOS, ce qui autorise des applications immédiates pour la vérification formelle et le prototypage rapide. La rapidité de la traduction et l'efficacité du code engendré permettent de traiter des programmes de taille significative avec de bonnes performances.

17h45 – 18h30

David Champelovier

Traian 3 : un compilateur pour la partie données des langages LOTOS et LOTOS NT

L'objectif de Traian 3 est de remplacer les outils actuels Caesar.adt et Traian 2, en compilant les types abstraits de données des langages LOTOS et LOTOS NT. Forts des expériences accumulées avec Caesar.adt et Traian 2, nous avons entrepris de répertorier un maximum de souhaits (requirements) pour Traian 3. Cet exposé en présente les points-clés.

Mercredi 11 Juin 2003

9h30 – 11h15

Frédéric Lang

Outils de vérification compositionnelle dans CADP

La vérification énumérative de systèmes concurrents doit faire face au problème bien connu d'explosion combinatoire d'états. La vérification compositionnelle est un moyen de pallier ce problème, consistant à :

·        décomposer la génération d'espace d'états du système à vérifier en la génération d'espaces d'états des sous-systèmes qui le composent;

·        appliquer à chacun de ces sous-systèmes des opérations réduisant leur taille (minimisation modulo des bisimulations  fortes ou faibles et abstractions basées sur la notion d'interface de synchronisation);

·        puis recomposer en parallèle les sous-systèmes ainsi réduits.

Cet exposé présentera un panorama des nouveaux outils de vérification compositionnelle qui seront intégrés dans la prochaine version  de la boîte à outils CADP.

11h45 – 13h15

Hubert Garavel et Christophe Joubert (travail commun avec Holger Hermanns)

Combiner vérification compositionnelle et évaluation de performances avec CADP

Il est souhaitable, à la fois pour des raisons scientifiques et économiques, de considérer la correction fonctionnelle et l'évaluation de performances dans un même cadre conceptuel. Nous décrivons comment la boîte à outils CADP, initialement conçue pour vérifier la correction fonctionnelle de spécifications LOTOS, peut aussi être utilisée  pour l'évaluation de performance. Nous présentons les nouveaux outils récemment ajoutés à CADP pour l'évaluation de performance. Nous illustrons l'approche proposée avec deux exemples : les stabilisateurs de vol du satellite Hubble et le protocole d'arbitrage du bus SCSI-2.

Déjeuner

14h45 – 15h45

Dominique Borrione (laboratoire TIMA, Grenoble)

Présentation des travaux du groupe VDS sur la vérification de systèmes matériels

15h45 – 16h30

Emil Dumitrescu (laboratoire TIMA, Grenoble)

La simulation symbolique comme stratégie de simplification pour la vérification de systèmes sur la puce par "model checking"

The successful application of model-checking to industrial designs requires methods for reducing the complexity of the model. We present an original strategy, for a well identified class of circuit behaviors; by running an appropriate symbolic simulation pattern before the actual proof of a temporal formula, an important FSM model simplification can be obtained. The actual model reduction step is formalized and illustrated. This method has been implemented within the CMU version of the SMV model checking tool and validated on a large industrial design.

17h00 – 17h45

Menouer Boubekeur (laboratoire TIMA, Grenoble)

Expérimentation de CADP pour la validation de spécifications de circuits asynchrones écrites en CHP

Cet exposé traite de l'analyse et la validation des spécifications de circuits asynchrones écrites en CHP. L'approche consiste à utiliser des formalismes et outils de vérification issus du domaine de la validation de logiciels, et notamment des systèmes distribués, dont le modèle d'exécution est similaire à celui des circuits asynchrones. Les spécifications CHP sont traduites dans le format intermédiaire IF basé sur des machines d'états communicantes à commande gardée. Elles sont ensuite validées en utilisant l'environnement IF/CADP, qui fournit des outils de model-checking et de bisimulation. L'exposé commence en introduction par les spécifications des circuits asynchrones ; il présente brièvement une première approche de validation basée sur les langages matériels (VHDL), ses avantages et ses inconvénients. Ensuite il développe l'approche basée sur l'utilisation de l'environnement IF/CADP pour la validation, Enfin, il se termine par une étude comparative des deux approches.

17h45 – 18h45

Solofo Ramangalahy (Bull)

Vérification fonctionnelle avec Exec/Caesar

Nous présentons les travaux en cours dans l'action Bull-Inria FormalFame sur la vérification de circuits. La méthode développée sur une étude de cas repose sur le compilateur Caesar de CADP et, notamment,  le schéma de compilation Exec/Caesar.

Jeudi 12 Juin 2003

9h30 – 10h45

Damien Bergamini

Introduction au modèle intermédiaire de Caesar

Cet exposé présente le modèle intermédiaire utilisé par le compilateur LOTOS Caesar, depuis la phase de génération jusqu'à la phase de simulation. Il décrit également les travaux effectués dans le cadre du projet Bull-Inria FormalFame  qui visent  à améliorer les performances de la phase de simulation, notamment en mode Exec/Caesar. L'exposé se termine par la présentation de quelques pistes de réflexion intéressantes dans l'optique de nouvelles optimisations.

10h45 – 11h30

Frédéric Lang

NTIF: un modèle symbolique général pour les processus séquentiels communicants comportant des données

Un problème central dans la vérification de systèmes composés de processus communicants séquentiels comportant des données est de trouver un modèle symbolique adéquat. Un tel modèle doit offrir une représentation compacte des flots de données et de contrôle. Il doit aussi être adapté pour des techniques de vérification telles que le ``model checking'' et la preuve de théorèmes. Un grand nombre de modèles ont été proposés, la plupart étant basés sur le paradigme des ``commandes gardées'' (également appelé ``condition/action''). Dans cet exposé, on montre les limites de ce paradigme et l'on présente un meilleur modèle, dénommé NTIF (New Technology Intermediate Form), qui est bien adapté à la compilation des langages concurrents de haut niveau (tels que la récente norme internationale E-LOTOS).

12h00 – 13h00

Aurore Collomb

Prise en compte des contraintes temporelles dans NTIF

Au travers d'un exemple d'exclusion mutuelle (algorithme de Fisher) nous montrons que les langages de modélisation doivent pouvoir exprimer des contraintes temporelles. Ces contraintes sont déjà intégrées dans les algèbres de processus temporisées ou les automates temporisés. L'exposé  analyse donc d'un côté les choix pris quant au temps dans les algèbres de processus temporisées et ceux pris pour les automates temporisés. Nous faisons alors le point sur les problèmes soulevés par l'introduction du temps dans un langage.  Puis l'exposé traite plus particulièrement de l'extension du langage NTIF par des actions temporisées en commençant par la présentation des choix de syntaxe et de sémantique. Ayant introduit une sémantique dynamique formelle temporisée, nous voyons qu'il est possible d'obtenir pour toute spécification NTIF un STE temporisé. Ceci nous permet alors de traduire les spécifications NTIF en automates temporisés pour des outils tels que TReX ou UPPAAL. Après une partie sur les traductions vers ces outils en cours, nous faisons le point sur  deux études de cas : l'algorithme de Fisher et l'étude d'une carte à puce (porte-monnaie électronique).

Déjeuner

14h30 – 15h

Hubert Garavel

Présentation des activités scientifiques du projet VASY

15h30 – 16h45

Hubert Garavel et Radu Mateescu

Panorama des fonctionnalités de la boîte à outils CADP

CADP est une boîte à outils pour le développement des systèmes asynchrones qui offre des fonctionnalités multiples : simulation, génération de code, génération de tests, vérification basée sur des logiques temporelles et des bisimulations, vérification compositionnelle, etc. Dans cet exposé, nous présentons les principes et l'architecture de CADP et nous faisons le point sur les récentes avancées. L'exposé sera accompagné de démonstrations d'outils pour une étude de cas (modélisation et vérification de circuits systoliques calculant un produit de convolution).

17h15 – 18h45

Frédéric Tronel

Le projet Parfums : Vérification compositionnelle d'un protocole distribué basé sur des agents Java

Le projet Parfums est un projet RNTL qui regroupe les sociétés Mge-Ups, Silicomp Research, ScalAgent et le projet Vasy de l'INRIA. Son but est la création d'une gamme d'onduleurs Mge-Ups qui puissent être gérés à distance, aussi bien en ce qui concerne la surveillance du matériel que la maintenance logicielle. Le logiciel capable de fournir de tels services est fourni par ScalAgent. Il s'exécute sur une carte embarquée conçue par Silicomp Research. Le projet Vasy, pour sa part, étudie le protocole sur lequel reposent les capacités du logiciel en termes de configuration et de déploiement.

Etant donné qu'il s'agit d'un protocole dont le comportement dépend de l'architecture à déployer, nous avons choisi d'écrire un compilateur qui, sur l'entrée d'un fichier XML décrivant l'architecture à déployer produit une spécification en langage Lotos du protocole correctement paramétré.

Afin de surmonter les différents problèmes d'explosion d'états survenus lors de nos expérimentations, nous avons choisi d'utiliser une méthode compositionnelle de génération du graphe d'accessibilité. Pour cela, nous avons eu recours au langage de script SVL, fourni par la boîte à outils CADP. Le compilateur réalisé lors de l'étude du protocole génère, en plus d'une description Lotos de l'ensemble des processus intervenant dans le protocole, un script SVL. Ce script regroupe à la fois les aspects d'un scénario de vérification adapté à l'architecture à déployer, ainsi que la description des interactions entre processus. Nous détaillerons l'ensemble des problèmes rencontrés lors de ce travail, ainsi que les solutions que nous avons pu apporter.

Vendredi 13 Juin 2003

9h00 – 10h30

Francois Fages et Nathalie Chabrier (INRIA Rocquencourt)

"Model checking" symbolique de réseaux biochimiques

La biologie s'est clairement engagée ces dernières années dans un travail d'élucidation des processus biologiques de haut niveau en termes de leurs bases biochimiques à l'échelle moléculaire.  Cet effort de désassemblage par identification et mesure de certaines caractéristiques des constituants élémentaires (gènes et protéines) commence à pouvoir servir de base à l'effort systématique inverse : la reconstitution des mécanismes biologiques au sein desquels ces constituants exhibent une fonction.

Dans cet exposé nous proposons l'utilisation de la logique temporelle CTL comme langage d'expression des propriétés biologiques d'un système. Nous montrons que les techniques de "model checking" symbolique s'appliquent aux réseaux biochimiques et qu'elles présentent certains avantages sur la simulation pour interroger et valider des modèles formels de processus biologiques. Nous dresserons un bilan de nos expériences sur l'utilisation du "model checker" symbolique NuSMV et du "model checker" avec contraintes DMC, sur la modélisation et l'interrogation de deux processus biochimiques: un modèle qualitatif du contrôle du cycle cellulaire chez les mammifères, et un modèle quantitatif de régulation de l'expression génique.

Nathalie Chabrier  fera une démonstration (en avant- première) du système BIOCHAM "The biochemical abstract machine".

11h00 – 12h30

Jean-Pierre Gallois, Christophe Gaston, Nicolas Rapin (CEA Saclay)

Analyse comportementale de spécifications formelles a base d'automates par dépliage

Nous proposons de présenter les fondements théoriques de l'outil AGATHA. L'objectif de cet outil est de fournir une aide aux ingénieurs en ce qui concerne l'activité de validation de spécifications, lorsqu'elles sont décrites sous forme d'automates étendus communicants. Le principe est d'exhiber tous les comportements  de la spécification sous la forme d'un nouvel automate étendu ayant une structure particulière : ce dernier a presque une structure d'arbre si ce n'est que certaines transitions dénotent une inclusion des "avenirs" de l'état source s1 dans les "avenirs" de l'état cible s2 (l'arborescence issue de s1 est incluse dans l'arborescence issue de s2).

Cet automate déplié a une structure qui le rend beaucoup plus lisible que l'automate initial et reste de taille raisonnable (i.e. peut être analysé par un être humain) grâce aux techniques d'exécution symboliques sous-jacentes à la technologie. D'un point de vue plus mathématique :

·        l'automate déplié a la même sémantique que l'automate initial,

·        il exhibe tous les états puits de la spécification,

·        le dépliage peut être effectué au niveau global sur un système composé de plusieurs automates communicants ou au niveau local, en composant les dépliages des sous-automates du système : ces deux approches commutent.

Lorsque la spécification est considérée comme étant correcte, les contraintes symboliques associées aux comportements sont exploitées pour dériver des tests numériques afin d'évaluer la conformité de l'implantation à sa spécification.

Jean-Pierre Gallois donnera des perspectives sur l'utilisation industrielle d'AGATHA ainsi qu'une démonstration sur Linux.

Déjeuner

14h – 16h

Radu Mateescu

MCL et EVALUATOR 4.0 : un langage et un outil pour la vérification des systèmes parallèles comportant des données

Les systèmes industriels critiques, tels que les protocoles de télécommunication, les logiciels embarqués ou les architectures multiprocesseurs, comportent souvent du parallélisme et des structures de données complexes. Pour décrire le comportement de tels systèmes, des langages adéquats (comme LOTOS et E-LOTOS) ont été normalisés par l'ISO.

En revanche, pour spécifier et vérifier leurs propriétés, les formalismes classiques (comme les logiques temporelles ou le mu-calcul modal) ne sont pas adéquats, car étant définis sur un vocabulaire d'actions atomiques, ils ne permettent pas de manipuler des actions structurées contenant des noms de portes et des valeurs typées.

Nous proposons un langage de spécification de propriétés appelé MCL (Model Checking Language) basé sur une extension du mu-calcul modal avec des mécanismes pour la manipulation des valeurs typées. MCL comporte des opérateurs modaux capables d'extraire les valeurs contenues dans les actions, des opérateurs de point fixe paramétrés par des variables typées, des expressions régulières étendues permettant d'effectuer des calculs sur les séquences d'actions, ainsi que des méta-opérateurs autorisant la spécification de propriétés non standard.

Nous présentons également l'outil EVALUATOR 4.0, qui effectue la vérification "à la volée" des propriétés exprimées en MCL. L'approche adoptée consiste à traduire le problème de la vérification vers la résolution locale d'un système d'équations booléennes, qui est effectuée au moyen de la bibliothèque générique CAESAR_SOLVE récemment développée au sein de l'environnement OPEN/CAESAR.

16h – 16h30

Alban Catry

Traduction de formules du mu-calcul en système d'équations booléennes en utilisant la technologie de compilation SYNTAX/TRAIAN

Dans le cadre du projet européen Archware, on cherche à vérifier des propriétés écrites dans un langage spécifique (AAL) basé sur du mu-calcul étendu avec des données. Pour cela, une phase de traduction est nécessaire pour passer de AAL à un format utilisable par la nouvelle bibliothèque de vérification de CADP (CAESAR_SOLVE); ce format est un code C intermédiaire décrivant la formule à vérifier sous forme d'un système d'équations booléennes. Cette traduction est faite avec les outils SYNTAX/TRAIAN, et utilise LOTOS NT comme langage de spécification.

16h30

Clôture