|
Séminaire VASY 2002
|
|
Programme scientifique
|
Mardi 29 Octobre 2002 |
|
|
9h30 |
Ouverture |
|
9h30 – 10h45 |
Aurore Collomb T-ReX: A tool for reachability analysis of extended automata
T-ReX permet l'analyse automatique (génération des états atteignables) de systèmes paramétrés par des compteurs et des horloges, communicant par synchronisation et par files d'attente non bornées avec perte. L’exposé explicite le fonctionnement de T-ReX en mettant l’accent sur les notions suivantes : représentation symbolique des compteurs et des horloges par des matrices de bornes paramétrées (PDBM), méthodes d'accélération permettant l'arrêt de l'algorithme d'analyse dans les cas périodiques, vérification de propriétés de sûreté et de vivacité. L’exposé se conclut par l'énoncé de résultats d'utilisation de T-ReX. |
|
11h15 –12h15 |
Damien Bergamini Génération automatique de tests repartis en utilisant des modèles de vrai parallélisme
Le test de conformité est une activité indispensable dans le cycle de développement des logiciels. Bien que l'on dispose déjà d'outils permettant de générer de manière automatique des tests pour les systèmes centralisés, il n'existe encore rien de comparable pour les systèmes répartis. La technique actuelle consiste à considérer le système réparti à tester non pas comme un ensemble d'entités s'exécutant en parallèle mais comme un système centralisé. Les tests produits de cette manière se révèlent malheureusement peu efficaces. En nous inspirant des travaux de Ulrich/König, Henniger et Jard, ainsi que des outils déjà existants dans le domaine du test centralisé, nous avons écrit une chaîne d'outils complète prenant en charge toutes les étapes du processus de génération des tests répartis. Cet outil prend en entrée une spécification formelle du système à tester et produit en sortie une suite de tests de conformité. L'application de cette suite de test au système permet d'établir un verdict quant à sa conformité ou sa non-conformité par rapport à la spécification. Notre outil confirme l'intérêt de l'utilisation de modèles dits de "vrai-parallélisme" pour la génération automatique de tests répartis. |
|
12h15 – 14h00 |
Déjeuner |
|
14h00 –15h00 |
Frédéric Tronel Le projet Parfums : Vérification d'un protocole distribué basé sur des agents Java
Le projet Parfums est un projet labélisé par le RNTL. Il regroupe Mge-Ups, Silicomp Research, ScalAgent et le projet Vasy. 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. Pour cela, nous avons développé un compilateur qui part d'une description XML de l'infrastructure gérée par le logiciel et la traduit en une spécification Lotos. Nous avons mis au point une stratégie de vérification compositionnelle permettant de surmonter les différents problèmes d'explosion d'états survenus lors de nos expérimentations. |
|
15h00 – 16h45 |
Jean-Bernard Stefani (Projet Sardes / INRIA Rhône-Alpes) The M-calculus: A higher-order distributed process calculus
We present a new distributed process calculus, called the M-calculus, which can be understood as a higher-order version of the Distributed Join calculus with programmable localities. The calculus retains the implementable character of the Distributed Join calculus while overcoming several important limitations: insufficient control over communication and mobility, absence of dynamic binding, and limited locality semantics. The calculus is equipped with a polymorphic type system that guarantees the unicity of locality names, even in presence of higher-order communications -- a crucial property for the determinacy of message routing in the calculus. |
|
17h15 – 18h45 |
Radu Mateescu Résolution générique à la volée de systèmes d'équations booléennes et applications
Les systèmes d'équations booléennes (SEB) offrent une représentation naturelle de divers problèmes de vérification sur les Systèmes de Transitions Etiquetées (STE), comme la vérification par équivalence ou préordre (equivalence checking) et par logique temporelle (model checking). En particulier, les méthodes de résolution de SEB dites ``à la volée’’ permettent de construire le SEB -- et, par conséquent, le(s) STE(s) à vérifier -- de manière incrémentale au fur et à mesure de la vérification. Dans cet exposé nous présentons une bibliothèque générique, appelée CAESAR_SOLVE, pour la résolution à la volée des SEB d'alternance 1 (c’est-à-dire qui ne comportent pas de récursion mutuelle entre les variables de plus petit et de plus grand point fixe). La bibliothèque comporte actuellement quatre algorithmes de résolution différents: les algorithmes A1 et A2 sont généraux (A2 étant optimisé pour produire des diagnostics de profondeur réduite), tandis que les algorithmes A3 et A4 sont spécialisés pour résoudre les SEB acycliques et les SEB disjonctifs/conjonctifs avec une consommation mémoire moindre. La bibliothèque CAESAR_SOLVE est développée au moyen de l'environnement générique OPEN/CAESAR pour l'exploration à la volée de STE et sert actuellement de moteur pour les outils à la volée BISIMULATOR et EVALUATOR 4.0, destinés respectivement à la vérification par équivalence comportementales et à l’évaluation de formules de mu-calcul régulier d'alternance 1. |
|
Mercredi 30 Octobre 2002 |
|
|
9h30 – 11h30 |
Gilles Barthe (Projet Lemme / INRIA Sophia) Tool-Assisted Specification and Verification of the JavaCard
Bytecode verification is one of the key security functions of the JavaCard architecture. Its correctness is often cast relatively to a defensive virtual machine that performs checks at run-time, and an offensive one that does not, and can be summarized as stating that the two machines coincide on programs that pass bytecode verification. We review the process of establishing such a correctness statement in a proof assistant, and focus in particular on the problem of automating the construction of an offensive virtual machine and a bytecode verifier from a defensive machine.
G. Barthe, P. Courtieu, G. Dufay, and S. Melo de Sousa. Tool-Assisted Specification and Verification of the JavaCard Platform. In H. Kirchner and C. Ringeissen, editors, Proceedings of AMAST'02, LNCS 2422, pp 41--59. ftp://ftp-sop.inria.fr/lemme/personnel/Gilles.Barthe/amast02.ps.gz et |
|
11h45 – 13h30 |
Hubert Garavel (joint work with Mihaela Sighireanu) Towards a Second Generation of Formal Description Techniques - Rationale for the Design of E-LOTOS
Process algebras are often advocated as suitable formalisms for the specification of telecommunication protocols and distributed systems. However, despite their mathematical basis, despite standardization attempts (most notably the Formal Description Technique LOTOS), and despite an ever growing number of successful case-studies, process algebras have not yet reached a wide acceptance in industry. On the other hand, description languages such as PROMELA or SDL are quite popular, although they lack a formal semantics, which should prohibit their use for safety-critical systems. In this paper, we seek to merge the ``best of both worlds'' by attempting to define a ``second generation Formal Description Technique’' that would combine the strong theoretical foundations of process algebras with language features suitable for a wider industrial dissemination of formal methods. Taking the international standard LOTOS as a basis, we suggest several enhancements, which fall into three categories: data part, behaviour part, and modules. Our work was initiated in 1992 in the framework of the ISO/IEC Committee for the revision of the LOTOS standard. Several of our suggestions have integrated into the revised standard E-LOTOS. The other suggestions are considered in the context of LOTOS NT, a variant of E-LOTOS for which a prototype compiler/model-checker is under development at INRIA. |
|
13h30 – 16h00 |
Déjeuner |
|
16h00 – 16h45 |
Frédéric Lang (travail conjoint avec Hubert Garavel) NTIF: un modèle symbolique général pour les processus séquentiels communicants
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). |
|
17h00 – 17h45 |
Aurore Collomb Algèbres de processus temporisées
L'exposé débute par un rapide survol des algèbres de processus non temporisées. Afin de permettre la description de systèmes temps réel, nous discutons ensuite de l'ajout du temps dans les algèbres de processus non temporisées. L'analyse des descriptions algébriques (temporisées ou non) peut se faire (au moins) de deux manières : par relation d'équivalence ou par ``model-checking’’. Nous détaillons alors, dans le cadre de quelques algèbres, les différents résultats liés à ces deux méthodes et, le cas échéant, les outils existants. |
|
18h00 – 18h30 |
Christophe Joubert Minimisation of mixed labelled transition systems modulo nondeterministic decisions
Ce projet de 3ème année de Magistère en Informatique s'inscrit dans la combinaison entre évaluation de performances et vérification fonctionnelle. Après une description succincte des systèmes de transitions étiquetées (STE) stochastiques et, plus généralement, des systèmes mixtes probabilistes/stochastiques, nous aborderons le problème de l’intégration d’outils d'analyse de performances au sein de CADP. En particulier, nous présenterons l'outil DETERMINATOR destiné à traduire des STE mixtes non-déterministes vers des chaînes de Markov à temps continu, lesquelles constituent le modèle standard pour l'analyse numérique de performances. |
|
18h30 – 19h00 |
Solofo Ramangalahy (Bull) Functional hardware verification
The problem of (functional) verification for hardware is briefly presented, from an industrial point of view. Then, the solutions adopted by the Accellera standardization organization are described, with an emphasis on the definition of PSL (Property Specification Language). We relate this to some of the verification of logical properties done within FormalFame on using properties. We conclude on the possible consequence of this standardization work for the next year. |
|
Jeudi 31 Octobre 2002 |
|
|
9h30 – 11h30 |
Hubert Garavel Parallel and Distributed Model-Checking
This lecture attempts to provide a comprehensive survey of the work done in the context of state space generation and analysis using parallel and distributed computing. The lecture encompasses various areas, including state space generation, equivalence checking, model checking, and performance evaluation. |
|
11h30 – 12h15 |
Christophe Joubert Techniques et outils pour la construction massivement parallèle de systèmes de transitions
Ce travail de DEA porte sur l'étude, la conception et la mise en œuvre d'algorithmes pour la génération massivement parallèle d'espaces d'états en vue du model-checking. Nous commençons par un état de l'art complet des travaux de recherche sur la génération parallèle de modèles. Ensuite, nous proposons des algorithmes pour la construction parallèle de modèles à partir de programmes décrits dans un langage de haut niveau, tel que LOTOS. Un aspect novateur de notre approche est la gestion distribuée des structures de données dynamiques (listes, arbres, etc.) entre plusieurs machines. Nous avons spécifié nos algorithmes en LOTOS et vérifié leurs propriétés de bon fonctionnement (absence de blocage, détection de terminaison, sûreté) au moyen de la boîte à outils CADP. Nous avons également réalisé une implémentation prototype de ces algorithmes dans l'outil Distributor de CADP. Les expérimentations sur une grappe de PC ont confirmé le bon fonctionnement de nos algorithmes et ont montré des gains de performance importants à la fois en mémoire et en temps d'exécution. |
|
12h15 – 13h00 |
Frédéric Lang Présentation de l’outil EXP.OPEN 2.0
EXP.OPEN est l’un des compilateurs de l'environnement OPEN/CAESAR et l’une des briques de base permettant la vérification compositionnelle dans CADP. EXP.OPEN permet de générer les fonctions de l'API OPEN/CAESAR pour des systèmes d’automates communicants décrits dans le langage EXP (expressions décrivant des réseaux de STE composés en parallèle via les opérateurs algébriques de parallélisme et de masquage de LOTOS). L’exposé présente la version 2 de EXP.OPEN, en cours de développement, qui est basée sur une extension conservative du langage EXP avec des opérateurs algébriques issus d'autres langages (algèbres de processus CCS, CSP et muCRL, norme internationale E-LOTOS). L'objectif est de permettre l'utilisation des outils de vérification compositionnelle de CADP aux utilisateurs de ces langages. Après une brève présentation du mécanisme de traduction des expressions de composition vers des systèmes à base de vecteurs de synchronisation (similaires à ceux utilisés dans les outils MEC et FC2, qui sont à la base de l'implémentation), on abordera les techniques de réduction de l'espace d'état pour la bisimulation de branchement en montrant l'intérêt de l'utilisation des vecteurs de synchronisation pour ce type d'analyse. L’exposé se concluera par des résultats expérimentaux concernant l'implémentation de l'outil. |
|
13h00 – 15h00 |
Déjeuner |
|
15h00 – 16h30 |
Discussion: Perspectives scientifiques VASY 2002-2003 Animation: Hubert Garavel, Radu Mateescu et Frédéric Lang |
|
16h30 |
Clôture |