2002 - 2003

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




Programme du jeudi 19 juin 2003


Relâche




Prévisions





Réunions précédentes (2002 - 2003)

5 juin 2003

Erich Grädel
Il était une fois dans l'ouest. Détermination, définissabilité et complexité de jeux à itinéraires. .

Once upon a time, two players set out on an infinite ride through the west. More often than not, they had quite different ideas on where to go, but for reasons that have by now been forgotten they were forced to stay together -- as long as they were both alive. They agreed on the rule that each player can determine on every second day, where the ride should go. After omega days, an infinite ride is completed and it is time for payoff. There were variants of this game where, after some number of days, one of the players would be eliminated (these things happened in the west) and the other was to complete the game by himself for the remaining omega days (a very lonesome ride, indeed).

Path games arise also in other contexts than the wild west. They have been studied in descriptive set theory, in the form of Banach-Mazur games, which are path games on the infinite omega-branching tree. An important issue in this context is determinacy (does one of the players have a winning strategy?) and its dependency on the topological properties of the winning condition. In a quite different setting, Pistore and Vardi have recently used path games for task planning in nondeterministic domains. Rather than determinacy (which is obvious for winning conditions in such applications), the main concern here are the algorithmic properties. It turns out that planning problems modeled by path games can be solved by automata-based methods.

Here we consider path games in a general, abstract setting, but with emphasis on definability and complexity issues. After a brief review of the classical results on determinacy of Banach-Mazur games, we discuss path games that are positionally determined, i.e., admit winning strategies that only depend on the current position, not on the history of the play. This will be used to determine the complexity of deciding the winner of path games with LTL winning conditions. Finally we will investigate definability issues. We are interested in the question how the logical complexity of defining a winning condition (a property of infinite paths) is related to the logical complexity of defining who wins the associated game (a property of game graphs). In particular, we will see that the winner of path games with LTL winning conditions is definable in CTL$^*$.

This is joint work with Dietmar Berwanger and Stephan Kreutzer.

24 avril 2003

Stéphane Riedweg
Logique temporelle et contrôle .

Par extension des logiques temporelles, je propose un cadre formel et unifié pour une large classe de problèmes de contrôle. Cette extension est obtenue par quantification des proposition atomiques.

En particulier, une telle extension pour le mu-calcul est considérée et permet de spécifier, par exemple, des critères d'optimalité du contrôle comme la permissivité maximale. Elle ne permet cependant pas le contrôle sous observation partielle. Pour cela, une version quantifié du loop-mu-calculus est proposée et permet, dans le cadre [AVW03] (Arnold,Vincent, Walukiewicz: Games for synthesis of controllers with partial observation), de synthétiser un contrôleur maximal permissif parmi les contrôleurs sous observation partielle, par exemple.

http://www.inria.fr/rrrt/rr-4793.html

10 avril 2003

Catalin Dima
Discrétisation non archimédienne des langages temporisés .

27 mars 2003

Richard Castanet
Test de robustesse .

20 mars 2003

Mirabelle Nebut
Réactions synchrones, spécification et analyse .

L'approche synchrone est dédiée à la conception des systèmes réactifs. Grâce à leur sémantique forte, des langages synchrones comme Esterel, Lustre et Signal permettent de spécifier le comportement des systèmes de manière abstraite et rendent possible leur validation formelle, cruciale dans le cas des systèmes critiques.

L'application aux programmes synchrones des méthodes de vérification concernant les systèmes infinis et les aspects numériques est fondamentale, mais plus ou moins directe. En effet l'utilisation d'horloges dans les spécifications donne aux variables un statut d'absence ou de présence. Dans le cas de Signal l'absence de variables est explicitée par une valeur spéciale, ce qui empèche l'interfaçage direct des outils aux techniques existantes.

L'exposé traitera de la manipulation de l'absence des variables synchrones, plus particulièrement dans les langages flot de données. Après une introduction au paradigme synchrone et à l'utilisation des horloges, on donnera un état de l'art du traitement de l'absence dans les sémantiques et les analyses synchrones. Ensuite on présentera un langage logique d'horloges appelé CL, basé sur une extension par des aspects numériques des horloges booléennes utilisées dans le contexte de la compilation Signal. On montrera que CL permet d'interfacer naturellement les modèles étendus avec l'absence explicite à des théories standard, de plusieurs manières.

13 mars 2003

Franck Pommereau
Modèles composables et concurrents pour le temps-réel .

Cet exposé porte sur des modèles explicitant la concurrence qui s'appliquent au domaine du temps-réel. Le point de départ est un modèle basé sur des réseaux de Petri colorés composables à la manière des termes dans les algèbres de processus.

Nous montrons comment introduire dans ce cadre une représentation du temps, appelée « temps causal », dont l'originalité consiste à utiliser l'expressivité du modèle pour représenter explicitement une horloge dans les systèmes à temporiser. Cette approche se révèle souple et agréable à utiliser ; de plus, les résultats pratiques sont prometteurs puisqu'il a été possible de vérifier automatiquement des systèmes ainsi modélisés avec de meilleures performances que des méthodes réputées (les automates temporisés avec les outils UPPAAL et Kronos).

Par ailleurs, nous montrons comment étendre le modèle de départ pour y introduire des opérateurs permettant de représenter la préemption, c'est-à-dire l'interruption définitive ou temporaire des processus d'un système.

La seconde partie de l'exposé présente les bases formelles sur lesquelles s'appuient les travaux ci-dessus. Il s'agit d'algèbres de processus dotées de la structure suivante : une algèbre de termes est munie d'une sémantique opérationnelle au moyen de règles SOS ; une algèbre de réseaux de Petri permet de donner aux termes une sémantiques dénotationnelle ; ces deux sémantiques sont prouvées cohérentes (elles définissent les mêmes évolutions).

6 mars 2003

Pierre Courtieu
Jakarta: un environnement de spécification et de preuve pour la plate-forme JavaCard .

La plate-forme Javacard est l'environnement pour la programmation des cartes à puces de nouvelle génération. Elle intègre (entre autre) sur une carte à puce les composants suivants: une machine virtuelle de type Java(Card) (JCVM), un vérificateur de bytecode (BCV). Le rôle du BCV est d'effectuer une analyse statique des programmes compilés en bytecode devant être charger sur la puce, et d'autoriser ou non ce chargement en fonction du résultat de cette analyse. L'analyse vérifie plusieurs propriétés:
  • "le programme ne provoquera pas d'erreur de type"
  • "Une applet ne créera jamais de pointeur vers un endroit non autorisé"
  • etc...
Je présenterai notre travail(*) concernant la spécification et certification de vérificateur de bytecode dans l'assistant de preuve Coq, et l'outil dédié que nous développons pour cela: Jakarta.

(*) en commun avec Gilles Barthe, Guillaume Dufay et Simao Melo De Sousa

27 février 2003

Tayssir Touili
Reachability analysis of Process Rewrite Systems: Application to the verification of multithreaded recursive programs .

We consider the verification problem of programs with unbounded (1) recursive procedure calls, and (2) dynamic creation of concurrent processes. Programs are modeled using term rewrite systems called PRS (for process rewrite systems). These models are more powerful than pushdown automata and Petri nets, two common models for reasoning about, respectively, recursive programs without process creation, and multi-threaded programs without recursive calls. A PRS can actually be seen as the nesting of prefix rewrite system and a multiset rewrite system.

We define a generic procedure which constructs a finite representation of the set of all reachable configurations of a given PRS, provided that its underlying multiset rewrite system is semilinear. We represent PRS reachability sets by means of a new class of tree automata with unbounded width. Our procedure can be instantiated in different ways leading to new reachability analysis procedures for PRS.

(Joint work with Ahmed Bouajjani)

13 février 2003

Sabine Pérès
CTL et les réseaux de régulation génétique : un exemple avec multi-stationnarité .

Le langage formel CTL permet d'exprimer dans une logique modale des propriétés d'un réseau de régulation génétique. Le système biologique choisi pour illustrer l'utilisation de ce langage formel est la production de mucus dans Pseudomonas aeruginosa, une bactérie mucoïde jouant un rôle important dans la mucoviscidose. Des biologistes de Rouen ont émis l'hypothèse que la production de mucus de cette bactérie était un phénomène épigénétique et ont proposé un ensemble de modèles. Les réseaux de régulation multivalués développés par René Thomas qui permettent d'étudier ce type de système, constituent la sémantique de cette approche formelle. A partir de cette sémantique, on peut écrire une formule en logique formelle exprimant qu'un phénomène est épigénétique. On vérifie formellement que la modélisation proposée satisfaisait cette formule. De plus, on peut proposer des scénarii pour confronter les modèles à l'expérimentation.
6 février 2003

Grégoire Sutre
Temporal-Safety Proofs for Systems Code .

We present a methodology and tool for verifying and certifying systems code. The verification is based on the lazy-abstraction paradigm for intertwining the following three logical steps: construct a predicate abstraction from the code, model check the abstraction, and automatically refine the abstraction based on counterexample analysis. The certification is based on the proof-carrying code paradigm. Lazy abstraction enables the automatic construction of small proof certificates. The methodology is implemented in BLAST, the Berkeley Lazy Abstraction Software verification Tool. We describe our experience applying BLAST to Linux and Windows device drivers. Given the C code for a driver and for a temporal-safety monitor, BLAST automatically generates an easily checkable correctness certificate if the driver satisfies the specification, and an error trace otherwise.

Joint work with Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar, George C. Necula and Westley Weimer.

30 janvier 2003

Frédéric Herbreteau
Hybrid Acceleration using Real Vector Automata .

This work addresses the problem of computing an exact and effective representation of the set of reachable configurations of a linear hybrid automaton. Our solution is based on accelerating the state-space exploration by computing symbolically the repeated effect of cycles in the automaton transition graph. The computed sets of configurations are represented by Real Vector Automata (RVA), the expressive power of which goes beyond that of the first-order additive theory of real and integer variables. This approach makes it possible to obtain in finite time sets of configurations that cannot be expressed as finite unions of convex regions. The main technical contributions of the paper consist in a powerful sufficient criterion for checking whether a hybrid transformation (i.e., with both discrete and continuous features) can be accelerated, as well as an algorithm for applying such an accelerated transformation on RVA. Our results have been implemented and successfully applied to several case studies, including the well-known leaking gas burner, and a simple communication protocol with timers.
23 janvier 2003

Bernard Berthomieu
Espaces d'états abstraits pour les Réseaux de Petri Temporels .

Les réseaux de Petri Temporels (ou de Merlin), étendent les réseaux de Petri par des intervalles temporels associés aux transitions du réseau. Leurs espaces d´états sont en général infinis, et à branchement infini, même lorsque le réseau est borné. On discutera de plusieurs abstractions finies pour les espaces d'états des réseaux Temporels bornés. On rappellera tout d'abord la construction classique dite "des classes d´états" [IFIP 83]. Cette construction fournit une abstraction préservant les propriétes LTL de l'espace d'états. On présentera ensuite une construction récente [TACAS 03] qui préserve ses propriétés de branchement, telles qu'exprimées en CTL* ou mu-calcul. Cette dernière abstraction produit un graphe de classes d´états (ou états abstraits) bissimilaire à l'espace d'états. Ces constructions, ainsi que d'autres, sont implantées dans l'outil Tina [TINA].
[IFIP 83] B. Berthomieu, M. Menasche, An Enumerative Approach for Analyzing Time Petri Nets, IFIP Congress 1983, North Holland. http://www.laas.fr/tina/papers/ifip83tex.ps.gz
[TACAS 03] B. Berthomieu, F. Vernadat, State class constructions for branching analysis of Time Petri Nets, TACAS 2003 (a paraitre) http://www.laas.fr/tina/papers/ascg.ps.gz
[TINA] http://www.laas.fr/tina
9 janvier 2003

Alain Griffault
Extension du langage AltaRica et compilation vers Lustre .

12 décembre 2002

David James Sherman
Yeast Pheremone Signalling Pathways : an example of protein-protein interactions in cascade .

5 décembre 2002

Fabrice Kordon
LfP: un langage pour la modélisation de systèmes répartis .

Depuis plusieurs années, nous menons des travaux dans le domaine du prototypage de systèmes répartis (modélisation, vérification, génération automatique de programmes). Nous observons que les solutions actuelles (principalement à base d'UML) ne sont pas suffisantes pour capturer la dynamique du comportement de tels systèmes. Le principal problème vient du fait que cette description est distribuée dans différents diagrammes (comportement, séquence, états, etc.) dont les relations ne sont pas strictement spécifiées.

Nous présentons l'état actuel de nos travaux en cours visant à intégrer les besoins des systèmes répartis dans une notation qui servirait de base à la génération automatique de squelettes de contrôle et à la vérification formelle de tels systèmes.

21 novembre 2002

Anatol Slissenko
Un cadre logique pour la vérification des systèmes temps réel .

Nous décrivons une classe de logiques des prédicats avec le temps explicite qui permettent de représenter d'une façon relativement simple les requis et le fonctionnement des programmes temps réel. Ces logiques sont indécidables. Cependant beaucoup de problémes réalistes se trouvent dans une classe décidable que nous avons introduite. L'exposé présente les logiques FOTL (first order timed logic) et une classe décidable de problèmes de vérification. La complexité théorique et pratique sera discutée ainsi que des questions ouvertes.

(Travail commun avec D. Beauquier, LACL, Paris 12)

24 octobre 2002

Claire Pagetti
Une extension temporisée d'AltaRica .

AltaRica est un langage de spécification de haut niveau développé au LABRI.

Nous proposons une extension temps réel du langage qui permet de manipuler le temps quantitatif. Cette extension formelle est à la fois syntaxique (grammaire élargie) et sémantique (sous forme de systèmes de transitions intefacés temporisés). Les résultats d'AltaRica classique sont conservés.

Une fois AltaRica temporisé défini, nous avons développé un algorithme de traduction d'un noeud AltaRica temporisé en un automate temporisé. Ce qui nous permet ensuite d'utiliser des traitements standards des automates temporisés. Nous avons notamment étudié des propriétés temporelles sur des systèmes en utilisant le model checker UPPAAL.

17 octobre 2002

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

10 octobre 2002

Catalin Dima
Problèmes théoriques de spécification et de vérification de systèmes temporisés .

Cet exposé sera divisé en deux parties. Dans la première partie je vais présenter plusieurs approches pour la spécification de systèmes temporisés à l'aide des expressions régulières. Puis je vais parler du problème d'atteignabilité "relationelle" dans les automates temporisés et de différentes approches pour le résoudre.
3 octobre 2002

Réunion de rentrée.

  • Présentation des nouveaux membres.
  • Bilan de l'activité de l'équipe.
  • Préparation du programme du GT.
26 septembre 2002

Davy Rouillard
Application de techniques de preuve assistée, pour la spécification, la vérification et le test.




Archives des années précédentes





Navigation




Last modified: Fri Nov 21 19:57:54 CET 2003