Groupe de travail

Modélisation et Vérification


Chers collègues,
Nous n'aurons pas de séminaire jeudi prochain (2007-07-26).
Jérôme,
========================================================================
La page du groupe de travail:
http://www.labri.fr/~leroux/seminaire/
========================================================================


Calendrier

Pour proposer un séminaire, le calendrier vous aidera à choisir une date disponible.

Précédents séminaires de la session

Date (YYYY-MM-DD)Orateur/AnimateurTitre
2007-06-28Thomas Brihaye (LSV, Cachan, France) A probabilistic semantic for timed automata
Like most models used in model-checking, timed automata are an ideal mathematical model to represent systems with strong timing requirements. In such mathematical models, properties can be violated, due to unlikely events. Following ideas of Varacca and Völzer in their LICS'06 paper, we aim at defining a notion of ``fair'' correctness for timed systems. For this purpose, we introduce a probabilistic semantics for timed automata, which ignores unlikely events, and naturally raises a notion of almost-sure satisfaction of properties in timed systems. We prove that the almost-sure satisfaction has a corresponding topological interpretation in terms of largeness of the set of paths satisfying the property. Moreover, we show PSPACE-Completeness for the LTL model-checking problem over finite computations.

Il s'agit d'un travail en collaboration avec Christel Baier, Nathalie Bertrand, Patricia Bouyer et Marcus Größer

2007-06-26Stéphane Demri (LSV, Cachan, France) Logiques pour la Spécification et Vérification
Dans cet exposé, je vais reprendre la présentation de ma soutenance d'habilitation centrée sur les
logiques pour la spécification et vérification. Ce sera l'occasion de rappeler la place des formalismes
logiques en informatique avec un éclairage particulier pour la vérification formelle et l'interrogation de
données. Parmi les sujets abordés plus en détail, on peut trouver les logiques temporelles avec mécanisme
de mémoire et les contraintes de régularité dans les graphes.

Plus de détails sont disponibles sur www.lsv.ens-cachan.fr/~demri/soutenance.php

2007-06-21Nicolas Caniart (LaBRI, Bordeaux, France) Accélération de l'algorithme Cegar
Le semi-algorithme de model-checking Cegar (Counter-example guided
abstraction refinement) connait un très vif succès au sein de la
communauté de la vérification. Il a permis de vérifier des systèmes de
taille conséquente et réaliste. Cependant, inhérent à sa nature de
semi-algorithme, il existe encore de nombreux cas, parfois triviaux,
dans lequel il se comporte mal, voir échoue.
Dans cette exposé, on commencera par redéfinir Cegar et expliquer
son fonctionnement. On mettra en suite en avant quelques exemples de
systèmes (très simples) sur lesquels l'algorithme se comporte de fa-
çon inappropriée. On proposera ensuite quelques solutions envisagées
pour améliorer le comportement dans l'algorithme, au moyen de techni-
ques d'accélération et d'interpolation.


2007-06-07Patrick Chervet (LaBRI, Bordeaux, France) Minimizing variants of visibly pushdown automata
The minimization problem for visibly pushdown automata (VPA) is
studied. Two subclasses of VPA are introduced: call driven automata,
and block automata. For the first class, minimization results are
presented unifying and generalizing those present in the
literature. A drawback of this class, and all the other classes
known till now, is that it is exponentially less succinct than
VPA. The second class, block automata, is introduced to address this
problem. These automata are as succinct as VPA. A minimization
procedure for them is presented that requires one additional
parameter to be fixed. An example of an exponential gain in
succinctness is presented.
2007-05-31Felix Klaedtke (ETH-Zentrum, Zurich, Switzerland) Don't Care Words with an Application to the Automata-based Approach for Real Addition
As already pointed out by Büchi, automata can be used to decide
certain first-order theories of linear arithmetic, like the
first-order theory over the reals with addition and the ordering.
Reals are represented as infinite words, and the automata are
recursively constructed from the formulas. This automata-based
approach for representing and manipulating sets of reals has also
applications in infinite-state model checking. However, analogous to
BDDs to represent finite sets, the sizes of the automata are an
obstacle in the automata-based set representation.

In this talk, I will show how so-called "don't cares sets" for BDDs
can be generalized to languages as a means to reduce the automata
sizes and how "don't care words" can be used to build a more efficient
automata-based decision procedure for real addition. A general result
about don't care words is that the minimal weak deterministic B"uchi
automaton with respect to a given don't care set with certain
restrictions is uniquely determined and can be constructed
efficiently. Our implementation LIRA uses don't care words and
outperforms other state-of-the-art tools.
2007-04-26Frédéric Herbreteau (LaBRI, Bordeaux, France) Hybrid Acceleration
Linear hybrid automata are convenient for modeling systems with both discrete and continuous features, and for checking that requirements are met by the model. However, since model-checking is undecidable for linear hybrid automata, existing verification techniques choose to over approximate state-space computation in order to guarantee its termination. We present an acceleration technique that only helps termination without guarantee, but preserves exactness of the computed state-space. It is based on the ability to compute the transitive closure of loops in the model. This appears to yield termination of state-space computation on several examples (but of course, not always). Our acceleration technique for loops is able to handle so-called "periodic loops". However, many loops are not periodic, hence our technique has been extended with reduction rules that transforms some non-periodic loops into periodic ones. In particular, we show a reduction rule for timed automata (a decidable subclass of linear hybrid automata) that transforms any timed loop into a periodic one. Since timed automata can be flattened (Comon and Jurski), these entails that their state-space is effectively computable using our approach.
2007-04-05Fabrice Chevalier (LSV, Cachan, France) Décidabilité et contrôle de logiques temps-réel
La logique temporelle MTL (Metric Temporal Logic) est une extension de LTL avec des contraintes quantitatives : elle permet par exemple d'exprimer qu'un événement se produira dans moins de 5 unités de temps. MTL a longtemps été supposée indécidable; ce n'est que récemment que Ouaknine et Worrel ont montré que la décidabilité de MTL dépend en fait de la sémantique considérée ("pointwise" ou "interval-based"). Nous revisiterons les résultats d'indécidabilité de MTL et étudierons la synthèse de contrôleur pour des spécifications MTL.
2007-03-22Nathalie Bertrand (Université de Dresden, Allemagne) Vérification des Lossy Channel Systems probabilistes et non-déterministes.
Dans les années 90, le modèle de Lossy Channel System (LCS) a été
introduit pour représenter des protocoles de communication par file
d'attentes imparfaites. Ce modèle a permis de vérifier des propriétés
de sureté pour des protocoles de communication asynchrone concus pour
pallier les pertes de messages. Néanmoins, il était trop pessimiste
concernant les questions de vivacité, car il introduisait des
comportements marginaux très peu probables (tels que l'exécution où
tous les messages sont systématiquement perdus).


Nous avons défini un modèle combinant probabilités et non-déterminisme
pour les LCS, dénoté NPLCS. Ce modèle permet de représenter les pertes
de messages comme des événements aléatoires, et les lectures ou
écritures dans les canaux par des choix non-déterministes. Nous avons
alors considéré le problème de la vérification qualitative, dont une
instance est par exemple : " existe-t-il un comportement
non-déterministe (appelé adversaire) pour lequel la probabilité de
vérifier une formule est positive ?". On montre que la vérification
qualitative est indécidable pour les NPLCS. Néanmoins, lorsqu'on
considère la classe raisonnable des adversaires à mémoire finie, la
vérification qualitative est décidable. Nous exposerons ces résultats
(indécidabilité et décidabilité), en détaillant en particulier les
ingrédients qui fournissent la décidabilité, à savoir : (1)
l'existence d'un attracteur fini, et (2) un théorème de convergence du
calcul itératif de certains points fixes.
2007-03-15Axel Legay (Institut Montefiore, Liege, Belgique) Sociable Interfaces: Theory, Implementation, and Future
Open systems are systems whose behavior is jointly determined by their internal structure, and by the inputs that they receive from their environment. A component of a larger system is, therefore, an open system, as its behavior depends on the inputs it receives from the other system components.

Since the last decades, various models have been introduce to model open systems. Among them one finds game-based models that represent the interaction between the behavior originating within a component, and the behavior originating from the component's environment as a game.

In this talk, I will first recall the basic advantages of using a game-based model for the specification, verification, composition, and refinement of open systems.

I will then introduce sociable interfaces, a recent concrete asynchronous game-based model where components have rich communication primitives that facilitate the modeling of software and distributed systems as well as global resources.

The Sociable Interfaces model has been implemented in a tool called TICC. I will describe the main features of TICC, and explain the difficulties of moving from the theoretical description of the model to its implementation.

Finally, I will discuss the possibility of adding time to the model.

Joint work with Luca de Alfaro and Marco Faella.
2007-03-08Pierre-Alain Reynier (LSV, Cachan, France) Dépliages temporisés de réseaux d'automates temporisés
Alors que les méthodes d'ordres partiels ont prouvé leur efficacité pour l'analyse de systèmes à événements discrets, leur application aux systèmes temporisés reste un sujet de recherche délicat . Nous proposons ici une méthode de vérification pour les réseaux d'automates temporisés avec invariants. Fondée sur la technique du dépliage, notre méthode produit un processus branchant, exprimé comme un réseau de Petri acyclique étendu avec des arcs de lecture. Ces arcs nous permettent d'obtenir une relation de concurrence entre les événements la plus large possible. D'autre part, nous attachons à chaque événement, en plus d'un marquage, une zone qui représente les contraintes temporisées associées à cet événement. Nous expliquons alors comment se limiter à une partie bornée de ces zones, correspondant au marquage de cet événement. Nous calculons enfin un préfixe fini et complet de ce dépliage, permettant de résoudre le problème de l'accessibilité.
2007-02-15Radu Iosif (VERIMAG, Grenoble, France) Flat Parametric Counter Automata
In this paper we study parametric flat counter automata and their relation with various
decidable fragments of integer arithmetic. We establish a hierarchy of flat counter automata,
by restricting the number of parameters, the number of loops and the form of the transition
relations. For each class in the hierarchy, we found a matching subtheory of integers, in the
sense that, for each automaton in the class, the reachability (emptiness) problem can be
expressed as the satisfiability of a formula in the language of a given theory, and viceversa.
Using the same arithmetic theories allowed us to also establish the relation of flat counter
automata with previous work on 2-way reversal bounded counter machines. Last, we report on an
effective procedure to answer the question whether a given 1-parametric linear Diophantine system
has a solution.
2007-02-01Nicolas Markey (LSV, Cachan, France) Verification of (One-clock) Priced Timed Automata
Priced timed (game) automata are timed (game) automata
extended with cost functions [ATP01,BFH+01]. The cost
functions are just "observers", and cannot act upon the
behavior of the automaton.

We consider two classical problems:
- computation of optimal cost and optimal winning strategies
in PTGAs,
- quantitative (w.r.t. costs) CTL model-checking in PTAs.
We show that they are undecidable in general for priced timed
automata, and prove that they are decidable when restricting
to one-clock PTAs.
2007-01-25Julien Bertrane (LIENS, Paris, France) Certification de la résistance des réseaux de programmes synchrones aux erreurs matérielles
Nous définissons un modèle de l'exécution des programmes
synchrones communicants tenant compte des imperfections matérielles
(désynchronisation des horloges, retards dans la transmission des
données). Ces imperfections étant inévitables, les programmes
incluent des techniques de robustesse qui permettent d'implémenter
leur spécification malgré ces défauts. Cependant, ces techniques
sont complexes, modifient fortement les programmes, et sont souvent
ajoutées "à la main". Nous proposons donc une analyse statique
(i.e. sur le code source et pas à l'exécution) et automatique,
basée sur la théorie de l'interprétation abstraite, permettant
de prouver formellement certaines de ces spécifications.
2007-01-18Kaninda Musumbu (LaBRI, Bordeaux, France) Graf and Saïdi97'algorithm : Construction of abstract state graph Revisited
Let given a system S and a property phi, the problem of model-checking is the verification of the formula S | = phi.
That requires
- the construction of a model (STE) of execution of the system
- a temporal logic
- evaluation of the satisfaction of the property on the model.
This method does not apply to the system having a infite number of states.
It has nevertheless the advantage of being entirely automatizable.
The abstraction is a technique of checking which consists in building a finite
model for a system having an infinite number of states. That makes it possible to verify the properties wished on the abstract model by model-checking.
The construction of an abstract model consists in defining an
abstract domain and building a system of transition on this domain.
Graf and Saïdi have proposed an automatic algorithm of connstruction of
abstraction which requires many obligation of proof.
The goal of the talk is to present a simplification of this construction.
2007-01-11Laure Gonnord (VERIMAG, Grenoble, France) Combining Widening and Acceleration in Linear Relation Analysis
Linear Relation Analysis is one of the first, but still one of
the most powerful, abstract interpretations working in an infinite
lattice. As such, it makes use of a widening operator to enforce the
convergence of fixpoint computations. While the approximation due to
widening can be arbitrarily refined by delaying the application of
widening, the analysis quickly becomes too expensive with the increase
of delay. Previous attempts at improving the precision of widening are
not completely satisfactory, since none of them is guaranteed to
improve the precision of the result, and they can nevertheless
increase the cost of the analysis. In this talk, we investigate an
improvement of Linear Relation Analysis consisting in computing, when
possible, the exact (abstract) effect of a loop. This technique is
fully compatible with the use of widening, and whenever it applies, it
improves both the precision and the performance of the analysis.
2006-12-14Antoine Miné (LIENS, Paris, France) L'analyseur statique Astrée
Astrée est un analyseur statique, basé sur l'interprétation abstraite, qui vérifie l'absence d'erreurs à l'exécution pour un sous-ensemble du langage C. Astrée est sûr par construction: un sur-ensemble des comportements est calculé. Astrée est spécialisé dans l'analyse de codes synchrones réactifs de contrôle commande où il est précis et rapide (preuve d'absence de débordements de tableaux et d'erreurs arithmétiques sur les entiers et les flottants pour une application avionique critique de 400 000 lignes en 14h). Dans cet exposé, nous présenterons la méthodologie de conception d'analyseur spécialisé par raffinement des abstractions. Nous expliquerons le fonctionnement et la structure modulaire d'Astrée et donnerons quelques exemples précis de domaines abstraits qu'il nous a fallu concevoir ou adapter, tout en motivant les choix sémantiques et algorithmiques.
2006-12-07Anca Muscholl (LaBRI, Bordeaux, France) Logics and automata with infinite alphabets
In this survey we give an overview of recent
results on logics and automata with infinite
alphabets. In this setting, we reason about
data word and data tree languages, where we allow
(in addition to usual regular operations) equality
tests on the infinite alphabet component.

At the beginning of the 90's, research on this
topic focused on automata models à la Kaminski/Francez,
and Neven/Schwentick/Vianu. However, the results obtained were
mostly about undecidability and noncomparability
of different automata models and of logics.

Motivated by applications in XML data reasoning
and in verification, recent work focused on
exhibiting restricted decidable logics with data. Some examples
are 1) two-variable FO logics with order and
successor over finite and infinite data words, 2) two-variable
FO logics with successor over data tree languages
(Bojanczyk et al.) and 3) fragments of LTL with freeze operator
(Demri/Lazic).
2006-11-30The Quang Tran (LaBRI, Bordeaux, France) Unfolding Concurrent Well-Structured Transition Systems
Joint work with Frédéric Herbreteau and Grégoire Sutre.
-------------------------------------------------------

In this work, our main objective is to combine partial-order methods with
verification techniques for infinite-state systems in order to obtain efficient
verification algorithms for concurrent infinite-state systems. This paper
presents a general framework for partial-order modeling and verification of
well-structured transition systems.

Firstly, McMillan has proposed a technique in the verification of
systems modelled with finite-state Petri nets [McM95]. This technique is based on the
concept of net unfoldings and a well-known partial-order semantics of Petri
nets. It construct only a finite complete prefix of the unfolding which
contains full information about the reachable states. The unfolding technique
has been later developed for other model of concurrency, e.g. Synchronous
Products of Transition Systems [ER99], High-Level Petri Nets [KK03], Extended
Finite State Machines [LI05]; and applied to other verification problems,
e.g. checking relevant properties of speed independent circuits [KKTV95], simple
branching time logic [Esp94].

Although the finite prefix obtained by unfolding technique avoids the
interleaving explosion, it is sometimes much larger than necessary. Several
works trying to resolve this problem can be classified into two types. The
first one is to give a more adequate criteria in truncating the unfolding, e.g.
based on a total order of trace [ER99], based on the symmetry of Petri Nets w.r.t
some notions [CGP01]; and the second one is to avoiding the unuseful
multiplication of a same labeled event when unfolding non-safe Petri nets
[KKKV05].

In our work, we model concurrent systems as synchronized
products of (heterogeneous) components, where the semantics of components is
given in terms of event structures. This allows us to benefit from the
intrinsic concurrency in each component. We propose event structures for
counters and queues, and we present an on-the-fly compositional unfolding
algorithm that computes event structures for synchronized products. For the
particular case of well-structured components, we give property-preserving
truncation criteria [FS01] on event structures in order to obtain effective decision
algorithms for the boundedness, termination and quasi-liveness problems.
Moreover, our technique for avoiding redundancy in the unfolding can also
resolving the irrelevant multiplication problem stated in [KKKV05].

We have implemented a tool, called ESU, for demonstrating the benefits of our
approach.

[CGP01] Jean-Michel Couvreur, Sébastien Grivet, and Denis Poitrenaud. Unfolding
of products of symmetrical petri nets. In ICATPN, pages
121-143, 2001.

[ER99] J. Esparza and S. Römer. An unfolding algorithm for synchronous
products of transition systems. In International Conference on Con-
currency Theory, volume 1664 of Lecture Notes in Computer Sci-
ence, pages 2-20, 1999.

[Esp94] Javier Esparza. Model checking using net unfoldings. Sci. Comput.
Program., 23(2-3):151-195, 1994.

[FS01]Alain Finkel, Ph. Schnoebelen: Well-structured transition systems everywhere!
Theor. Comput. Sci. 256(1-2): 63-92 (2001)

[KK03] Victor Khomenko and Maciej Koutny. Branching processes of highlevel
petri nets. In TACAS, pages 458-472, 2003.

[KKKV05] Victor Khomenko, Alex Kondratyev, Maciej Koutny, and Walter
Vogler. Merged processes - a new condensed representation of petri
net behaviour. In CONCUR, pages 338-352, 2005.

[KKTV94] Michael Kishinevsky, Alex Kondratyev, Alexander Taubin, and Victor
Varshavsky. Analysis and identification of speed-independent
circuits on an event model. Formal Methods in System Design,
4(1):33-75, 1994.

[LI05] Yu Lei and S. Purushothaman Iyer. An approach to unfolding asynchronous
communication protocols. In FM, pages 334-349, 2005.

[McM95]Kenneth L. McMillan. A Technique of State Space Search Based on Unfolding. Formal Methods in System Design 6(1): 45-65 (1995).
2006-11-16Philippe Darondeau (IRISA, Rennes, France) Implementations distribuees du controle superviseur a la Ramadge et Wonham par synthese de reseaux de Petri
La theorie du controle superviseur de Ramadge-Wonham
permet, pour divers types de problemes de controle
poses en termes de langages reguliers, de decider si
ces problemes sont faisables, et de construire alors
des automates finis realisant le controle. Diverses
extensions de la theorie portent sur le controle des
systemes decentralises mais le controle des systemes
asynchrones et distribues reste un probleme ouvert.

Nous montrons comment integrer la synthese de reseaux
de Petri et la theorie de Ramadge-Wonham afin d'avoir
une reponse partielle a ce probleme.
2006-11-09Joel Ouaknine (Oxford University Computing Laboratory, Oxford, England) The Cost of Punctuality
In an influential paper titled "The Benefits of Relaxing Punctuality" (JACM 1996), Alur, Feder, & Henzinger introduced the logic Metric Interval Temporal Logic (MITL), which is a fragment of the real-time logic Metric Temporal Logic (MTL) in which the time constraints on operators are not allowed to be punctual, i.e., singleton sets. They produced an intricate proof (11 pages) that MITL model checking and satisfiability are decidable -- in fact EXPSPACE-COMPLETE. This has led to considerable further work; in the last year alone, both Hirshfeld & Rabinovich, and Maler, Nickovic, & Pnueli, published new and simpler decision procedures for MITL.

An obvious question to ask is, what happens if punctuality is allowed? Until recently, it was widely believed that the faintest presence of punctuality in any linear-time timed temporal logic would automatically lead to undecidability. Although this was recently disproved, until now no decidable punctual fragment of MTL was known to have even primitive recursive complexity (with certain fragments having provably non-primitive recursive complexity!).

Very recently, in joint work with Patricia Bouyer, Nicolas Markey, and James Worrell, we have been able to precisely pinpoint the complexity of the main decidable punctual fragments of MTL. Our complexity bounds involve a connection between MTL formulas and reversal-bounded Turing machines. We will present an overview of these results and how they relate to standard (untimed) verification.
2006-10-19Morgan Magnin (IRCCYN, Nantes, France) Réseaux de Petri à Chronométre - temps dense ou temps discret ?
L'utilisation croissante (dans lÆindustrie automobile mais aussi aéronautique) de réseaux informatiques embarqués implique de vérifier a priori leur bon fonctionnement. Il convient ainsi de développer des formalismes permettant d'écrire et de valider les interactions entre les activités des processeurs et les réseaux de communication. Les réseaux de Petri temporels sont un de ces formalismes. Ils permettent de modéliser la durée de différentes actions sous la forme d'un intervalle de temps. Ils peuvent par ailleurs être enrichis afin de représenter des tâches susceptibles d'être suspendues puis relancées.

Deux approches peuvent alors être considérées. La première consiste à considérer le temps comme une grandeur continue (c'est-à-dire que le système peut changer d'état à n'importe quel moment), la seconde à l'envisager comme une grandeur discrète (la progression du temps est assurée par l'occurrence de tics d'horloge et le système ne peut alors évoluer qu'à des instants précis). Notre objectif durant cette thèse est de comparer ces deux approches : nous souhaitons dégager les spécificités de chacune et déterminer les différentes propriétés qu'elles permettent de vérifier. Ces recherches théoriques s'accompagnent d'un volet pratique. En effet, nous implantons nos résultats dans Roméo, un logiciel d'analyse de systèmes embarqués, et assurons ainsi leur valorisation auprès du tissu industriel.
2006-10-12Blaise Genest (IRISA, Rennes, France) On Zielonka's Theorem and its Application to Verification
The well-known algorithm of Zielonka describes how to transform automatically a sequential automaton into a deterministic (distributed) asynchronous trace automaton. A straigthforward application is synthesis/implementation of distributed system. It can also be applied to obtain deadlock-free systems. We show here another application in terms of Dynamic and Distributed Verification. Unfortunately, Zielonka's algorithm gives an asynchronous automaton that is doubly exponential in the number of processes (and simply exponential in the size of the automaton), which implies that the verification takes an exponential time to be performed. We show how we improve the generic Zielonka's algorithm, which in particular yields a polynomial time complexity for the distributed verification. Non deterministic Implementation will also be considered.
2006-10-05Igor Walukiewicz (LaBRI, Bordeaux, France) Réunion de rentrée du thème Modélisation Vérification
Igor Walukiewicz animera la réunion.


Archives des années précédentes



Responsable

Jérôme Leroux first.last@labri.fr