2004 - 2005

Groupe de travail

Modélisation, Vérification et Test de systèmes informatisés

Le jeudi de 11h à 12h15
Salle 300, IMB, UFR de Mathématiques




Séance du jeudi 30 juin 2005


Relâche




Prévisions





Réunions précédentes (2004 - 2005)


23 juin 2005
Hugo Gimbert (LIAFA, Paris)
Équilibres de Nash stationnaires dans les jeux stochastiques à information parfaite
Dans cet exposé, on s'intéressera aux équilibres de Nash dans les jeux stochastiques multijoueurs à nombre fini d'états et à information parfaite.

Une partie d'un de ces jeux est constituée d'une succession infinie de tours de jeu. À chaque tour , le jeu est dans un ceratin état et un des joueurs choisit une action, qui détermine les transitions de probabilités vers le nouvel état. Pour choisir son action, chaque joueur se réfère à sa stratégie. Après une infinité de tours de jeu, chaque joueur reçoit une somme d'argent, calculée par une fonction de paiement en fonction de la suite infinie des états et des actions vus pendant la partie. Chaque joueur essaye naturellement de maximiser la somme qu'il reçoit. Un équilibre de Nash est une situation d'équilibre dans laquelle aucun des joueurs ne peut changer unilatéralement de stratégie sans diminuer son espérance de gain.

On exhibera une grande famille de fonctions de paiement pour lesquelles il existe des équilibres de Nash en stratégies stationnaires (i.e. positionnelles ou encore sans mémoire), équilibres qu'on peut calculer.

Ce travail s'appuie en partie sur les articles suivants:

  • "Stochastic Games", Shapley, 1953.
  • "Stay-in-a-set Games", Secchi et Sudderth, 2001.
  • "On Nash Equilibria in Stochastic Games", Chatterjee and Majumdar and Jurdzin'ski, 2003.
  • "Discounted Stochastic Games: the Finite Case", Sorin, 2003.
  • "Discounting Infinite Games but How and Why ?", G., Zielonka, 2004.
9 juin 2005
François Laroussinie (LSV, Cachan)
Model Checking Durational Probabilistic Systems
We consider model-checking algorithms for durational probabilistic systems, which are systems exhibiting nondeterministic, probabilistic and discrete-timed behaviour. We present two semantics for durational probabilistic systems, and show how formulae of the probabilistic and timed temporal logic PTCTL can be verified on such systems. We also address complexity issues, in particular identifying the cases in which model checking durational probabilistic systems is harder than verifying non-probabilistic durational systems.

This work was done in collaboration with Jeremy Sproston.

19 mai 2005
Rémi Morin (LIF, Marseille)
Raffinements au pays des MSC
Nous présenterons différentes approches adoptées pour l'étude de la réalisabilité de spécifications sous forme de langages de scénarios du type MSC (Message Sequence Charts). Nous détaillerons une technique de synthèse décomposée sous la forme de trois rafinements successifs à partir d'une spécification régulière. Cette décomposition suggère un problème plus général de contrôle de systèmes distribués.
21 avril 2005
Christophe Kehren (CERT-ONERA, Toulouse)
Modèles d'architectures de sûreté (automates AltaRica de propriétés)
L'objectif de ce travail est de proposer des méthodes et outils assistant la modélisation et l'évaluation de l'architecture de sûreté de fonctionnement des systèmes embarqués complexes. Ces méthodes et outils sont basés sur des modèles généraux d'architectures de systèmes correspondant à des éléments de sûreté. Un tel modèle d'architecture de sûreté (MAS) est une solution récurrente qui décrit et résout un problème général dans un contexte particulier. Le but est, entre autre, d'appliquer l'approche design patterns en génie logiciel au domaine de la sûreté de fonctionnement ce qui, à notre connaissance, n'a pas encore été réalisé. En effet, les design patterns proposent des solutions à des problèmes récurrents, renseignent sur les conséquences et le contexte d'utilisation et proposent des noms génériques aux patterns permettant de définir un vocabulaire précis.

Une définition rigoureuse des modèles d'architectures de sûreté a tout d'abord permis de préciser leur contenu. Ils renferment un ensemble d'hypothèses, une spécification correspondant à l'architecture de l'élément de sûreté qu'est censé représenter le MAS et enfin des exigences garanties qui vont dépendre à la fois des hypothèses et de l'architecture. La finalité de cette définition est également de définir un ensemble d'attributs dans le but de distinguer les différents MAS par un nom générique et une structure propre leur conférant certaines propriétés sous certaines hypothèses. Ces attributs permettent de capitaliser le savoir d'experts des différents domaines d'utilisation ainsi qu'une meilleure utilisation/choix des solutions lors de la phase amont de conception d'architectures. Pour faciliter cette conception, un catalogue de MAS a également été réalisé. Après avoir défini les besoins et les solutions appropriées de manière informelle, nous nous sommes intéressés à la manipulation de ces modèles et donc à leur formalisation.

Le comportement des systèmes en présence de pannes peut être formalisé à l'aide de langages formels comme AltaRica, développé au Laboratoire Bordelais de Recherche en Informatique. En effet, le langage AltaRica est dédié à la modélisation orientée sûreté de fonctionnement et les modèles AltaRica peuvent être compilés vers des formalismes connus et analysés à l'aide d'outils existants. AltaRica nous permet de réaliser un modèle opérationnel (i.e. simulable) d'un système. Dans notre cas, les MAS correspondent à des abstractions d'architectures et donc requièrent une modélisation plus déclarative, i.e. à l'aide de propriétés. Ces propriétés étant en général dynamiques, nous avons choisi la Logique Temporelle Linéaire pour les modéliser. La description des modèles d'architectures de sûreté est donc constituée d'une partie AltaRica et d'une partie LTL. Ce type de modélisation mixte n'existe pas à notre connaissance et possède plusieurs intérêts, notamment lors de la conception en phase amont d'architectures de systèmes où il est possible de considérer qu'une partie du système est clairement définie et qu'une autre partie ne l'est pas complètement ou en cours d'étude. Cette dernière correspond à un MAS. Nous avons donc défini une notation mixant de l'opérationnel (AltaRica pour les composants bien définis) et du dénotationnel (une variante de LTL pour les composants spécifiés à partir de propriétés).

Les liens étroits avec AIRBUS France nous ont permis de valider globalement notre l'approche sur des modèles AltaRica de systèmes avion (génération hydraulique et électrique de type A320).

14 avril 2005
Jérôme Leroux (IRISA, Rennes)
De l'automate binaire à la formule de Presburger
Number Decision Diagrams (NDD) are the automata-based symbolic representation for manipulating sets of integer vectors encoded as strings of digit vectors (least or most significant digit first). Since 1969, we know that any Presburger-definable set (a set of integer vectors satisfying a formula in the first-order additive theory of the integers) can be represented by a NDD, and efficient algorithm for manipulating these sets have been recently developed. However, the problem of deciding if a NDD represents such a set, is a well-known hard problem first solved by Muchnik in 1991 with a quadruply-exponential time algorithm. In this paper, we show how to determine in polynomial time whether a NDD represents a Presburger-definable set, and we provide in this positive case a polynomial time algorithm that constructs from the NDD a Presburger-formula that defines the same set.
7 avril 2005
Karen Godary (CITI, Lyon)
Validation temporelle de TTA, architecture embarquée tolérante aux fautes pour l'automobile
La tendance actuelle dans l'automobile est au développement des systèmes X-by-wire : remplacement de la mécanique par de l'électronique embarquée. Ces systèmes supportent des applications distribuées critiques et temps-réel, typiquement comme une application de freinage. Ces systèmes possèdent des contraintes importantes de temps et de fiabilité qui ont imposé le développement d'architectures spécifiques tolérantes aux fautes telles TTA, FlexRay ou TTCAN. Dans le contexte de ces applications critiques, il est alors nécessaire de valider la tolérance aux fautes de ces architectures.

Notre étude s'est portée sur la validation temporelle de l'architecture TTA (Time Triggered Architecture). Nous avons proposé une méthodologie de vérification des bornes temporelles des services de TTA (comme par exemple l'initialisation), c'est à dire de leur pire temps d'exécution sous certaines hypothèses de fautes. Cette méthodologie est basée sur la modélisation de l'architecture en automates temporisés, sur l'abstraction de ce modèle pour réduire l'explosion combinatoire de l'analyse, puis sur la vérification de propriétés par model checking (par l'outil UPPAAL). Une seconde étape permet l'extraction des bornes temporelles paramétrées des services de TTA.

31 mars 2005
Olivier Ly (LaBRI)
Compositional Verification: Decidability Issues Using Graph Substitutions
Nous nous intéressons à la vérification compositionnelle de programmes séquentiels. Il s'agit de décider de façon algorithmique si un ensemble de propriétés locales structurelles des fonctions composant un programme donné implique une propriété globale de l'exécution de ce dernier.

Nous nous intéressons en particulier aux propriétés exprimées dans le langage de la logique monadique du second ordre concernant le graphe de flot de contrôle du programme, ainsi que des appels de fonctions.

Nous montrons que le problème de la compositionnalité est décidable pour les programmes dont les graphes de flot de contrôle sont de largeur arborescente bornée, ce qui notamment est le cas des programmes structurés.

Formellement, cela revient à montrer la décidabilité des théories MSO des familles d'hypergraphes obtenues par substitutions uniformes d'hyperarcs, substitutions spécifiées elles-même dans le langage MSO.

NB: J'ai déjà donné cet exposé au groupe de travail "Graphes et Logique" l'an passé.

17 mars 2005
The Quang Tran (LaBRI)
Unfoldings of Well-Structured Transition Systems
Formal verification and especially automatic formal methods have been intensively studied for verification of system correctness. But two of its greatest problems are state space explosion for finite-state systems and undecidability of verification properties for infinite-state systems.

Some techniques, so called partial-order techniques, have been proposed to solve the first problem. They all use independence between some of the system's operations to have more concurrency on the behavioral level of the system. Among them, McMillan's unfolding technique is an efficient technique for finite systems modeled by Petri nets.

The second problem can be avoided by considering only subclasses of infinite-state systems. Finkel and Schnoebelen have proved the decidability of some interesting problems for the "well-structured transition systems" subclass. However their technique is based on a structure called finite reachability tree where concurrency is ignored.

Our work thus aims at solving verification problems on infinite concurrent systems by combining these two techniques.

Work supervised by F. Herbreteau and G. Sutre.

17 février 2005
Mikolaj Bojanczyk (LIAFA, Paris)
Decidable characterisations of tree logics
Given a class L of regular languages of finite trees, the following decision problem may be considered: decide if the language recognized by a given tree automaton belongs to L.

I will begin with an overview of some instances of this problem, in cases where L is defined in a logical fashion (for instance when L is the class of languages defined in first-order logic).

Then I will concentrate on a decision procedure for the case where L corresponds to the temporal logic TL(EF), where the only temporal operator is EF (exists finally).

Joint work with I. Walukiewicz.

3 février 2005
Danièle Beauquier (LACL, Créteil)
Décidabilité du model-checking de systèmes temps-réel probabilistes
Une logique probabiliste avec un temps explicite sera présentée ainsi que des résultats de décidabilité du model-checking de cette logique appliqué à des chaînes de Markov. Une extension partielle au cas des processus semi-Markoviens et aux automates temporisés sera donnée.
27 janvier 2005
André Arnold (LaBRI)
Présentation du logiciel Synthesis de Gérald Point
9 décembre 2004
Kais Klai (LaBRI)
Réseaux de Petri : vérification modulaire et symbolique
Dans cette présentation, je présenterai certains de mes travaux concernant la vérification de systèmes concurrents modélisé par des Réseaux de Petri. Deux types d'approches seront abordés:
  1. Les approches structurelles par décomposition de réseau,
  2. Les approches comportementales basées sur une représentation symbolique des comportements du système.
Trois approches jouant sur des aspects orthogonaux seront présentées.

Dans la première approche, nous abordons la décomposition du réseau de Petri en sous réseaux, tirant profit de synchronisations par fusion de transitions pour préserver le comportement originel. Nous proposons une technique de vérification ramenant la vérification d'une propriété sur le système global à une vérification modulaire sur des parties du système.

Dans la deuxième approche, nous proposons une méthode de vérification purement comportementale. Cette méthode est basée sur la construction d'un graphe réduit à partir de l'observation des actions (transitions) apparaissant dans la formule à vérifier. Ce graphe est appelé graphe d'observation et est basée sur l'exploitation des Diagramme de décision binaires (BDD): chaque noeud du graphe abstrait un sousgraphe codé par un BDD et qui abstrait un ensemble de marquages ordinaires connectés par des actions non observées.

La troisième technique de vérification est une technique mixte visant à combiner les deux premières de manière à tirer profit des points forts de chacune.

2 décembre 2004
Thao Dang (VERIMAG, Grenoble)
The d/dt tool for verification of hybrid systems
We describe the reachability analysis methods implemented in the tool d/dt. This tool allows to verify safety properties of continuous and hybrid systems. For linear continuous systems with uncertain input of the form $dx/dt=Ax+bu$, the reachability computation algorithm is based on a technique for over-approximating reachable sets by convex and orthogonal polyhedra. This algorithm was also extended in various directions. One extension involves the verification of systems that admit mode switching and are modeled by hybrid automata. Another extension handles nonlinear continuous systems of the form $dx/dt=f(x)$. This extension is based on partitioning the state space into simplices and assigning a distinct discrete state to each of them. The continuous dynamics at each state is approximated by an affine function that interpolates the values of $f$ at the vertices the corresponding simplex.

In addition to verification, the tool allows to automatically synthesize a controller which switches the system between continuous modes in order to satisfy a safety specification. The synthesis algorithm uses a variant of the reachability methods to derive an under-approximation of the maximal invariant set.

(This work was done in collaboration with Eugene Asarin, Olivier Bournez, Antoine Girard, and Oded Maler)

18 novembre 2004
Sébastien Grivet (LaBRI)
Dépliages efficaces de réseaux de Petri
Le dépliage permet de représenter les états accessibles d'un système concurrent. Pour éviter l'explosion combinatoire liée au nombre d'états, cette technique tire parti de l'indépendance des événements. On montre que le temps et l'espace nécessaires pour son calcul, dépendent essentiellement des détails de son implémentation. Différentes solutions sont proposées pour les améliorer. On étend aussi les travaux qui cherchent à réduire le nombre d'états explorés. Tout ceci nous conduit à développer une méthode qui applique des stratégies spécifiques aux systèmes utilisés.
4 novembre 2004
Jean-Michel Couvreur
Sur une proposition de projet INRIA
28 octobre 2004
Shweta Gehlot (LaBRI)
Verification of Systems with Data and Control Operations with Symbolic Simulation and Validity Checking
Exhaustive verification of safety critical systems is of utmost importance in today's world. Such systems often use both data and control intensive sub-systems. This makes it extremely difficult to verify them using traditional approaches. Formal verification techniques like model checking and theorem proving are often not sufficient by themselves to verify such systems efficiently. Model Checking, in particular, is impractical for verifying data-intensive applications, where state space is very large. Theorem proving, on the other hand can be applied to verify such systems but requires a great degree of manual intervention. Symbolic simulation, is known to be effective in verification of such systems. Symbolic simulation can support detailed system models and can handle system descriptions as well.

Some popular circuit-level symbolic simulators developed by the research community are COSMOS, Voss and a unnamed simulator from Stanford university. COSMOS and Voss are based on a simulation technique called symbolic trajectory evaluation (henceforth STE). The major limitation of STE is that the temporal logic for specification of properties is quite restricted. This problem constrains the applicability of this approach for verifying complex properties of data and control intensive systems. On the other hand, the simulator developed by the Stanford research group is based on guiding symbolic simulation using weak reachability invariants. This simulator is reported to handle circuits having complex control and data path operations. Unfortunately, it is not available publicly and requires a significant amount of manual intervention for guiding the simulation.

In this background, our work is an attempt to develop a tool for verification of data and control intensive systems specified at the structural VHDL level using symbolic simulator and powerful validity checking engine. This allows us to reason about systems that are both data and control intensive in a semi-interactive way.

21 octobre 2004
Blaise Genest (University of Warwick)
A Kleene-Büchi Theorem for a class of communicating automata with effective algorithms
Using regular sets of representatives gives a unified way to do model-checking for infinite-state communicating formalisms. We give a theorem which describes exactly the models which have a particular regular set of representatives, in term of communicating automata, MSO logical formulas and MSC-graphs. These different formalisms are thus expressively equivalent, giving an extension of Kleene-Büchi theorem for communicating formalisms.

Joint work with Dietrich Kuske and Anca Muscholl.

14 octobre 2004
Jean-Michel Couvreur (LaBRI)
Simple determinization of Büchi automata accepting weak w-languages
We analyse the determinization problem for Büchi automata recognizing weak w-languages, which are the languages that are recognizable by deterministic weak Büchi automata. We show that the power set construction used in the finite word case, may be simply adapted for this subclass of w-languages. Then, for weak w-languages, given a nondeterministic Büchi automaton with n states, the equivalent deterministic weak automaton has at most 2^n states.
7 octobre 2004
Alain Griffault
Sur l'extension d'AltaRica
30 septembre 2004
André Arnold
Réunion de rentrée
Ordre du jour :
  • Présentation des nouveaux membres.
  • Bilan et perspectives des activités de l'équipe.
  • Préparation du programme du GT.
SéminaireDiscussionRelâche



Archives des années précédentes





Navigation




Last modified: Thu Jun 30 17:48:15 CEST 2005