2001 - 2002

Groupe de travail

Modélisation, Vérification et Tests des systèmes informatisés
&
Petite école pour la vérification

Le jeudi de 10h45 à 12h
Salle G.T. 2, LaBRI, Rez-de-chaussée




Calendrier (2001 - 2002)





Réunions de l'année 2001 - 2002

30 mai 2002

Alain Griffault
AltaRica : syntaxe et sémantique .

23 mai 2002

Luigi Santocanale
Induction, Co-induction, et jeux de parité .

Un jeu de parité est joué sur un graphe fini de positions et de mouvements. Dans ce graphe on peut bien avoir des cycles, et pourtant on définit l'ensemble des chemins inifinis gagnants pour un des deux joueurs à l'aide de la ``condition de parité''. Cette condition est bien connue dans la théorie des automates qui reconnaissent les objects infinis. En effet tout automate est équivalent à un automate qui utilise la condition de parité. Nous allons définir cette condition et lui donner une interprétation algébrique à l'aide des notions d'algèbre initiale et coalgèbre finale d'un foncteur, c-à-d., à l'aide des formulations catégorielles de l'induction et de la coinduction. Nous allons associer une expression algébrique à chaque jeu de parité et montrer qu'elle dénote (dans la catégorie des ensembles) l'ensemble des stratégies gagnantes pour un des deux joueurs. Nous montrons aussi que les expressions associés aux jeux sont équivalentes aux expressions qu'on peut engendrer par les operations de produit fini, de coproduit fini, d'algèbre initiale et coalgèbre finale, c.à-d aux µ-termes catégoriels. Nous obtenons cette façon une caractérisation explicite de tous les foncteurs qu'on peut définir par des µ-termes dans la catégorie des ensembles.
16 mai 2002

Sardaouna Hamadou
ASET : Un protocole anonyme et sécuritaire pour les transactions électroniques .

Nous présentons dans ce travail, un protocole de transaction électronique sécuritaire et surtout anonyme par l'association d'un logiciel de cryptage et d'une carte à puce. La sécurité est assurée par l'utilisation des techniques cyptographiques telles que le chiffrage, la signature électronique et l'authentification. L'anonymat est assuré par le fait que le client ne révèle au marchand aucune information pouvant l'identifier tout en garantissant la quasi-impossibilité d'une fraude.
18 avril 2002

Jean-Claude Royer
Type Abstrait Graphique .

Une préoccupation actuelle en spécification concerne les systèmes mixtes ou hétérogènes, i.e. des systèmes avec à la fois des aspects dynamiques et des types de données. Ce problème apparaît en spécification formelle mais aussi dans le contexte des méthodes de développement comme UML par exemple. Dans ce domaine nous avons proposé le couplage d'un système de transition symbolique et d'une spécification algébrique que nous avons appelé Type Abstrait Graphique. Nous montrons les principes de la spécification sur un exemple simple de distributeur de boisson et nous commenterons quelques propriétés de la spécification produite. Nous aborderons ensuite une approche basée sur la logique du premier ordre et permettant d'écrire des propriétés de logique temporelle et d'en faire la preuve en utilisant par exemple Larch Prover ou PVS. En dernier lieu nous esquisserons quelques liens connus avec la logique temporelle CTL* et quelques résultats concernant l'automatisation des preuves.
11 avril 2002

Michaël Adélaïde
Analyse paramétrique des systèmes hybrides .

Les systèmes hybrides permettent de modéliser des processus dont le comportement est une succession d'évolutions continues et de transitions discrètes. Les applications mises en oeuvre en Informatique Temps-Réel en font partie. Etant donnée une spécification des contraintes P à réaliser, le designer représente les applications sous la forme d'automates hybrides. Avant la mise en service de ces programmes, il est nécessaire de vérifier que les contraintes sont été respectées. Les outils de la vérification "traditionnelle" renvoient des réponses booléennes : les contraintes sont ou ne sont pas respectées. Pour l'analyse paramétrique, les constantes du système (vitesses, délais,...) ne sont pas fixées dès le départ. Le problème à résoudre est de trouver les valeurs de ses constantes pour lesquelles la propriété P est vérifiée.
La première approche consiste à paramétrer l'outil permettant de vérifier les systèmes sans paramètres. On peut définir un processus mécanique pour cette transformation. Il consiste à utiliser des types qui correspondent à la "non-évaluation" des formules sur le type original. Si on veut paramétrer des entiers sur lesquels on n'effectue que l'addition et la multiplication, on utilise l'anneau des polynômes à coefficients entiers (les inconnues étant les paramètres). Cependant, les restrictions suivantes apparaissent :
  • Cela n'est pas toujours possible, des problèmes non décidables peuvent apparaître ce qui réduit la classe d'automates que l'on peut paramétrer. Ainsi, il n'existe pas d'algorithme déterminant les solution entières d'un polynôme de degré quelconque ayant plus de deux inconnues.
  • L'outil paramétré est un semi-algorithme dans le cas général.
Il faut alors classer les problèmes (décidables, non décidables) dans le cas paramétré. Les premiers résultats sont négatifs pour l'analyse d'accessibilité :
  • elle n'est pas décidable pour les automates temporisés paramétrés alors qu'elle l'est dans le cas non paramétré (Alur, 1993),
  • elle n'est pas décidable pour les automates initialisés à pente rectangulaires paramétrés alors qu'elle l'est dans le cas non paramétré (Hong Toi, 1999).
Enfin, la classe des automates (paramétrés) faiblement contrôlés est présentée. Un algorithme est donné pour résoudre le problème de l'accessibilité (Adélaïde, Roux, soumis à AMAST 2002).
4 avril 2002

Bernard Boigelot
On the Use of Weak Automata for Deciding Linear Arithmetic with Integer and Real Variables .

This talk introduces finite-automata based algorithms for handling linear arithmetic with both real and integer variables. Previous work has shown that this theory can be dealt with by using finite automata on infinite words, but this involves some difficult and delicate to implement algorithms. The contribution of this work is to show, using topological arguments, that only a restricted class of automata on infinite words are necessary for handling real and integer linear arithmetic. This allows the use of substantially simpler algorithms. These algorithms have been implemented in a verification tool for programs relying both integer and real variables.
Joint work with S. Jodogne and P. Wolper.
21 mars 2002

Giacomo Lenzi
The D'Agostino-Hollenberg Uniform Interpolation Theorem for the Mu Calculus .

We consider modal mu calculus, a logic introduced by Kozen in 1983. Modal mu calculus is the extension of modal logic with two operators which give the least and greatest fixpoints of monotone functions from sets to sets. Modal mu calculus is considerably expressive, and it is widely used in system verification. Recall that a logic is said to ``have interpolation'' if for every two formulas A, C with A => C (where => denotes logical implication), there is an ``interpolant'' formula B in the common language of A and C such that A => B => C. For instance, first order logic has interpolation.
However, mu calculus not only has interpolation, but it has also a stronger property called ``uniform interpolation'': that is, for every formula A and for every language L, there is a ``uniform interpolant'' formula I(A,L), in the language L, such that:
  1. A => I(A,L), and
  2. for every formula C in the language L, if A => C, then I(A,L) => C.
That Mu Calculus has uniform interpolation is a theorem of D'Agostino and Hollenberg. It has been published in the paper: Giovanna D'Agostino and Marco Hollenberg, Logical questions concerning the $\mu$--Calculus: interpolation, Lyndon and Los - Tarski. Journal of Symbolic Logic, vol. 65, no. 1, March 2000, pp 310--331.
In this talk we will present this theorem, we will sketch the proof, and we will give some motivations, applications and related work.
14 mars 2002

Ahmed Bouajjani
TReX: A Tool for Reachability Analysis of Complex Systems .

We present a tool for automatic analysis of infinite-state systems modeled by means of extended automata. The models that can be analysed are parametric clocks and counters automata communicating through lossy FIFO-channels. The tool, called TREX, uses symbolic representations for infinite-state domains (regular expressions, parametric DBMs, arithmetical constraints), and forward/backward reachability analysis procedures, enhanced with acceleration techniques in order to help termination. TREX allows on-the-fly verification of safety properties, the generation ofthe reachability set which can be used, e.g., for parameter synthesis and for invariant generation, and the construction of a finite symbolic graph which can be used for finite-model checking. The tool is interfaced with the IF environment allowing to use SDL as a specification language, and to interact with abstraction tools and finite model-checkers.
Travail commun avec Aurore Annichini-Collomb et Mihaela Sighireanu.
21 février 2002

Jean-Michel Couvreur
Sur les dépliages de réseaux de Petri (suite) .

14 février 2002

Jean-Michel Couvreur
Sur les dépliages de réseaux de Petri .

7 février 2002

Alain Finkel
Accélérer permet de terminer ! .

Calculer effectivement une représentation symbolique de l'ensemble des états accessibles d'un système paramétré ou infini est une question centrale en vérification. Nous étudierons des modèles indécidables en général mais pour lesquels les accélérations sont quand même calculables. Nous montrerons que l'utilisation du cadre des accélérations et des représentations symboliques permet de verifier un certain nombre de protocoles bien connus. L'outil FAST, en cours de développement, a permis de réaliser des expériences très encourageantes sur la plupart des protocoles de diffusion (broadcast protocols).
31 janvier 2002

Vlad Rusu
Verification using test generation techniques .

Applying formal methods to testing has recently become a popular research topic. In this talk we demonstrate the opposite approach, namely, applying testing techniques to formal verification. The idea is to use symbolic test generation techniques to extract subgraphs (called "components") from a specification and to perform the verification on the components rather than on the whole system. This may considerably reduce the verification effort and, under reasonable sufficient conditions, a safety property verified on a component also holds on the whole specification. We demonstrate the approach by verifying an electronic purse system using our symbolic test generation tool STG and the PVS theorem prover.
URL: http://www.irisa.fr/pampa/perso/rusu/draft/
24 janvier 2002

André Arnold
Synthèse de contrôleurs (suite) .

17 janvier 2002

Franck Cassez
A Comparison of Control Problems for Timed and Hybrid Systems .

In the literature, we find several formulations of the control problem for timed and hybrid systems. We argue that formulations where a controller can cause an action at any point in dense (rational or real) time are problematic, by presenting an example where the controller must act faster and faster, yet causes no Zeno effects (say, the control actions are at times 0, 1/2, 1, 1 . 3/4, 2, 2 . 7/8, 3, 3 . 15/16, ...). Such a controller is, of course, not implementable in software. Such controllers are avoided by formulations where the controller can cause actions only at discrete (integer) points in time. While the resulting control problem is well-understood if the time unit, or ``sampling rate'' of the controller, is fixed a priori, we define a novel, stronger formulation: the discrete-time control problem with unknown sampling rate asks if a sampling controller exists for some sampling rate. We prove that, surprisingly and unfortunately, this problem is undecidable even in the special case of timed automata.
Joint work with Tom Henzinger (EECS Department, University of California at Berkeley, USA) and Jean-François Raskin (Département d'Informatique, Université Libre de Bruxelles, Belgium). To appear in HSCC'02.
10 janvier 2002

Claude Jard
Principes pour synthétiser des cas de test répartis en utilisant un modèle de "true-concurrency" .

La synthèse de cas de test pour le test de conformité de composants communicants a été principalement tournée vers la production de cas de test séquentiels. Dans le contexte des systèmes répartis, il est utile d'étendre ces techniques pour générer des testeurs multiples. Nous fondons ce travail sur notre expérience dans l'utilisation de techniques de model-checking, implantées avec succès dans l'outil TGV (Irisa/Vérimag) de génération de tests. Dans le prolongement des travaux de A. Ulrich et H. König, nous proposons d'utiliser un modèle de vrai-parallélisme basé sur le dépliage de graphes. La conférence présente les principes d'une chaîne complète de synthèse, depuis la définition d'objectifs de test jusqu'à la production d'un test projeté sur un ensemble de testeurs.
20 décembre 2001

Eugene Asarin
Bruit et décidabilité dans les systèmes hybrides .

Many properties of hybrid systems are algorithmically undecidable. In practice however, systems are only known up to a certain degree of accuracy and are subject to noise and perturbations. I will consider various classes of hybrid systems and will analyse how noise affects decidability for these classes. This presentation will be based on recent attempts by Asarin-Bouajjani, Henzinger-Raskin and others to formalize the impact of noise on computational capabilities of hybrid systems.
6 décembre 2001

Frédéric Herbreteau
Automates à file réactifs embarqués .

Les systèmes réactifs évoluent suivant les sollicitations (événements discrets) de leur environnement. La programmation asynchrone de telles applications nécessite de mémoriser les événements qui ne peuvent pas être traités lorsqu'ils surviennent. Les automates à file réactifs (AFR) permettent de modéliser de telles applications.
Qu'il s'agisse d'implantation ou de vérification, il est alors important de s'assurer de la bornitude de ces automates. Bien entendu, cette propriété dépend du rythme des occurrences des événements. Cette dernière spécification fait défaut aux AFR, c'est pourquoi, nous considérons les automates à file réactifs embarqués, qui comblent cette lacune.
Nous étudions divers problèmes de vérification pour les AFR embarqués, et en particulier, nous montrons que le problème de la bornitude est généralement indécidable. Ceci nous conduit à définir un test pour ce problème. Nous considérons ensuite la spécification de l'environnement sous la forme d'un système hybride, et nous adaptons notre test dans ce contexte.
29 novembre 2001

Bertrand Tavernier (CRIL Technology)
Plate-forme Calife : Utilisation d'XML pour un modèle commun .

22 novembre 2001

Kaninda Musumbu
Alose (avec ses arêtes) .

Alose (Automatisation de Logigrammes de Securité) est un simulateur de systèmes de sécurité écrit en Java exploité par une interface graphique écrite en Java Swing. Son usage est destiné à la vérification de systèmes de sécurité déjà existants ou en cours de conception. Ces fonctionnalités font de ce simulateur un outil qui permet de vérifier la cohérence d'un système de sécurité. L'exposé a pour objet de présenter la base théorique d'ALose.
15 novembre 2001

Patrick Félix
CALIFE et test .

Calife (Environnement pour la Preuve formelle et le Test d'Algorithmes utilisés en Télécommunication) est un projet de recherche RNRT dont l'objectif est de développer un prototype offrant un environnement pour la spécification, la vérification formelle et la génération de tests de systèmes avec des contraintes temporelles. Un modèle de spécification, appelé p-automates (une variante des systèmes hybrides linéaires) a été développé dans le cadre du projet Calife pour exprimer un système. Une des contributions de l'équipe concerne l'intégration d'outils de générations de séquences de tests dans cette plate-forme commune.
Les approches de génération automatique de séquences de test temporisées peuvent de décomposer selon les trois catégories suivantes :
  1. Génération à la volée selon un objectif de test,
  2. Génération à partir d'un graphe de région réduit,
  3. Approche assistant de preuve.

Cet exposé traitera des points 1 et 2. Le point 3 sera abordé lors d'un autre exposé (Davy Rouillard) dans le cadre de ce groupe de travail.
8 novembre 2001

Alain Griffault
Première "vraie" expérience d'utilisation du modèle AltaRica et de ses outils dans un contexte industriel .

25 octobre 2001

Aymeric Vincent
Synthèse de contrôleurs et stratégies gagnantes dans les jeux de parité .

Cette présentation se base sur un article publié à MSR 2001 et montrera le lien qui unit le problème de la synthèse de contrôleurs et le calcul d'une stratégie gagnante dans un jeu de parité.
18 octobre 2001

André Arnold
Synthèse de contrôleurs des systèmes à événements discrets .

I. La théorie de Ramadge et Wonham.
11 octobre 2001

Grégoire Sutre
Lazy abstraction .

One approach to model checking software is based on the abstract-check-refine paradigm: build an abstract model, then check the desired property, and if the check fails, refine the model and start over. We introduce the concept of lazy abstraction to integrate and optimize the three phases of the abstract-check-refine loop. Lazy abstraction continuously builds and refines a single abstract model on demand, driven by the model checker, so that different parts of the model may exhibit different degrees of precision, namely just enough to verify the desired property. We present an algorithm for model checking safety properties using lazy abstraction and describe an implementation of the algorithm applied to C programs.
4 octobre 2001

André Arnold
Réunion de rentrée .

  • Présentation des nouveaux membres.
  • Bilan de l'année et des projets en cours.
  • Perspectives de recherche.
  • Préparation du programme du premier semestre.



Archives des années précédentes





Navigation




Last modified: Tue Sep 17 19:40:57 CEST 2002