Groupe de travail

Modélisation et Vérification


Chers collègues,
Nous n'aurons pas de séminaire jeudi prochain (2008-07-31).
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.


Liste de diffusion

Pour s'abonner ou se désabonner de la liste de diffusion.

Précédents séminaires de la session

Date (YYYY-MM-DD)Orateur/AnimateurTitre
2008-06-12Jean-Francois Raskin (ULB, Brussels, Belgium) Fixpoint-based Abstraction Refinement and an Application to the converability problem for Petri Nets
In this talk, we present an abstract fixpoint checking algorithm with
automatic refinement by backward completion in Moore closed abstract
domains. We study the properties of our algorithm and prove it to be
more precise than the counterexample guided abstract refinement
algorithm (CEGAR). Contrary to several works in the literature, our
algorithm does not require the abstract domains to be partitions of
the state space. We also show that our automatic refinement technique
is compatible with so-called acceleration techniques.
Then, we show how to develop, from this general algorithm, an abstract interpretation
based analysis that reduces the dimensionality of state spaces that are
explored during verification of Petri nets. The dimensionality is reduced
by trying to gather places that may not be important for the property to
establish. If the abstraction that is obtained is too coarse, an automatic
refinement is performed and a more precise abstraction is obtained. The
refinement is computed by taking into account information about the
inconclusive analysis. The process is iterated until the property is proved
to be true or false.
2008-05-22Nathalie Bertrand (IRISA, Rennes, France) On decision problems for Probabilistic Büchi Automata
Probabilistic Büchi automata (PBA) are finite-state acceptors for infinite words where all choices are resolved by fixed distributions and where the accepted language is defined by the requirement that the measure of the accepting runs is positive. In this work we describe a complementation operator for PBA and a discuss on several algorithmic problems for PBA. All interesting problems, such as checking emptiness or equivalence for PBA or checking whether a finite transition system satisfies a PBA-specification, turn out to be undecidable. An important consequence of these results are several undecidability results for stochastic games with incomplete information, modelled by partially-observable Markov decision processes (POMDP) and $omega$-regular winning objectives. Furthermore, we study an alternative semantics for PBA where it is required that almost all runs for an accepted word are accepting, which turns out to be less powerful, but has a decidable emptiness problem.

This is a joint work with Christel Baier and Marcus Groesser.
2008-04-17Delphine Longuet (Centrum voor Wiskunde en Informatica (Netherlands)) Test de systèmes dynamiques à partir de spécifications modales
Parmi d'autres techniques de vérification et de validation, le
test est une méthode très largement utilisée pour assurer la qualité des
systèmes informatiques. Lorsque l'implantation du système n'est pas
connue, celui-ci peut être testé par rapport à une spécification formelle
ou informelle. Utiliser une spécification formelle comme référence de
correction du système permet de formaliser le processus de test et ainsi
de faciliter son automatisation. On distingue classiquement deux approches
du test à partir de spécifications formelles : les spécifications logiques
sont utilisées pour tester les comportements fonctionnels d'un système,
tandis que la dynamique est testée à l'aide de modèles à base d'états tels
que les systèmes de transitions. On montrera dans cet exposé de quelle
façon l'approche du test à partir de spécifications logiques, lorsqu'on
considère des spécifications exprimées en logique modale, peut être
utilisée pour tester des systèmes dynamiques.
2008-04-10Tristan Le Gall (IRISA, Rennes, France) Treillis abstraits et alphabets infinis
Cet exposé propose de voir les langages réguliers avec un alhabet fini ou infini comme un treillis. Ce treillis est utilisé, dans le cadre de l'interpréstation abstraite, pour vérifier des systèmes avec des files ou des piles non bornées.

Si les langages réguliers avec un alphabet fini sont bien connus, des problèmes de représentation et de manipulation surgissent quand l'alphabet est infini. J'introduirai la notion d'automates de treillis, qui sont semblables aux automates finis mais dont les transitions sont étiquetées par des éléments d'un treillis atomique infini.

Je détaillerai les opérations de déterminisation et de minimisation sur ce type d'automate et j'expliquerai comment on peut définir un opérateur d'élargissement. Je présenterai aussi quelques résultats expérimentaux.

En collaboration avec Bertrand Jeannet

2008-03-27Grégoire Sutre (LaBRI, Bordeaux, France) Accelerated Data-flow Analysis
Acceleration in symbolic verification consists in computing the exact effect of some control-flow loops in order to speed up the iterative fix-point computation of reachable states. Even if no termination guarantee is provided in theory, successful results were obtained in practice by different tools implementing this framework. In this talk, we show how to extend the acceleration framework to data-flow analysis. Compared to a classical widening/narrowing-based abstract interpretation, the loss of precision is controlled here by the choice of the abstract domain and does not depend on the way the abstract value is computed. We illustrate our approach on convex polyhedral data-flow analysis, and we provide a cubic-time acceleration-based algorithm for solving interval constraints with full multiplication.
Joint work with Jérôme Leroux.
2008-03-20Nicolas Caniart (LaBRI, Bordeaux, France) Accelerating Interpolant-based Model-checking
Interpolation-based model-checking and acceleration techniques
have been widely proved successful and efficient for reachability
checking. Surprisingly, these two techniques have never been combined
to strengthen each other. Intuitively, acceleration provides under-
approximation of the reachability set by computing the exact effect
of some control-flow cycles and combining them with other
transitions. On the other hand, interpolation-based model-checking is
refining an over-approximation of the reachable states based on
spurious error-traces.
In this talk we present a technique to combine acceleration
with interpolation-based model-checking at the refinement stage.
Our method, called “interpolant acceleration”, helps to refine the
abstraction, ruling out not only a single spurious error-trace but a
possibly infinite set of error-traces obtained by any unrolling of
its cycles. Interpolant acceleration is also proved to strictly
enlarge the set of transformations that can be usually handled by
acceleration techniques.
2008-03-13Patricia Bouyer (LSV, Cachan, France) Probabilities in Timed Automata
In this talk I will present a probabilistic semantics for timed automata, that allows to measure the likelihood of properties in a timed systems. I will then describe an abstraction that can be used to verify almost-surely LTL properties, and I will present limits of the approach. I will then turn to quantitative aspects, and present an approximation scheme that can be used to compute the probabilities of LTL properties in a timed automaton.
This is based on joint works with Christel Baier, Nathalie Bertrand, Thomas Brihaye, Nicolas Markey and Marcus Groesser.
2008-03-06Helmut Seidl (Institut für Informatik (Garching Germany)) On the Relationship between Interval Analysis and Mean Payoff Games
In a paper at ESOP 2007, we have presented an algorithm
for precise interval analysis based on strategy iteration.
While practically observed run-times are quite decent,
precise upper and lower complexity bounds have been unknown.
In this talk, we clarify the relationship of precise interval
analysis to mean-payoff games. In particular, we show that
mean-payoff games are polynomially equivalent to a class of
total-payoff games which in turn are equivalent to simple
integer equations. Since the latter form a sub-class of interval
equations, this means that proving precise interval analysis to
be polynomial is at least as hard as proving mean-payoff games
to be polynomial - which would solve a long-standing open problem
in theoretical computer science.

This work is an extension of joint work with Thomas Gawlitza
and based on late night discussions with Marcin Jurdzinski and
Uri Zwick at Dagstuhl.
2008-02-14Hugo Gimbert (LaBRI, Bordeaux, France) Jeux avec observation partielle
Dans un jeu avec observation partielle,
les joueurs prennent leurs décisions sans connaître l'état exact du système,
ils n'ont accès qu'à des signaux émis lors des changements d'état.

Le calcul des valeurs et des stratégies optimales de ces jeux
se révèle beaucoup plus ardu que dans le cas des jeux avec information parfaite:
au cours de cet exposé, nous présenterons plusieurs résultat
d'indécidabilité et de calculabilité, certains classiques, d'autres
récents ou inédits.
2008-02-07Andrey Rybalchenko (Max Planck Institute for Software Systems, Saarbrücken, Germany) path invariants
The success of software verification depends on the ability to find a
suitable abstraction of a program automatically. We propose a method
for automated abstraction refinement which overcomes some limitations
of current predicate discovery schemes. In current schemes, the cause
of a false alarm is identified as an infeasible error path, and the
abstraction is refined in order to remove that path. By contrast, we
view the cause of a false alarm ---the spurious
counterexample--- as a full-fledged program, namely, a fragment of
the original program whose control-flow graph may contain loops and
represent unbounded computations. There are two advantages to using
such path programs as counterexamples for abstraction
refinement. First, we can bring the whole machinery of program
analysis to bear on path programs, which are typically small compared
to the original program. Specifically, we use constraint-based
invariant generation to automatically infer invariants of path
programs ---so-called path invariants. Second, we use path
invariants for abstraction refinement in order to remove not one
infeasibility at a time, but at once all (possibly
infinitely many) infeasible error computations that are represented by
a path program. Unlike previous predicate discovery schemes, our
method handles loops without unrolling them; it infers abstractions
that involve universal quantification and naturally incorporates
disjunctive reasoning.
2008-01-24Bernard Boigelot (Institut Montefiore, Liege, Belgique) A Generalization of Cobham's Theorem to Automata over Real Numbers
Joint work with Julien Brusten.

This work studies the expressive power of finite-state automata
recognizing sets of real numbers encoded positionally.
Those automata can be used as data structures for representing the sets of
values that have to be handled during state-space exploration of systems
relying on integer and real variables, such as timed or hybrid automata.
It is known that the sets that are definable in the first-order additive
theory of real and integer variables ( R, Z, +, leq) can
all be recognized by weak deterministic Büchi automata, regardless of
the encoding base r geq 1. In this paper, we prove the reciprocal
property, i.e., that a subset of R that is recognizable by
weak deterministic automata in every base r geq 1 is necessarily
definable in ( R, Z, +, leq ). This result generalizes to real numbers
the well-known Cobham's theorem on the finite-state recognizability
of sets of integers. Our proof gives interesting insight into the
internal structure of automata recognizing sets of real numbers, which
may lead to efficient data structures for handling these sets.
2008-01-17Fares Chucri (LaBRI, Bordeaux, France) CEGAR Model-Checking pour AltaRica
Le Model Checking est une technique permettant de vérifier si une propriété est satisfaite par un système.
Il présente l'avantage de produire une trace de tout comportement indésirable (décrit par une expression logique) du système. Mais cette méthode présente l'inconvénient d'exploser en mémoire (the state explosion problem).
L'approche CEGAR (CounterExemple Guided Abstraction Refinement) permet de vérifier un système en utilisant une abstraction
finie de ce dernier. Grâce à cette approche il est possible de vérifier des gros systèmes et des systèmes infinis.
Une implémentation de la méthode CEGAR pour les modèles AltaRica à été rélisée dans Mec V, afin de comparer cette approche par
rapport aux méthodes de vérifications exhaustives classiques.
2007-12-13Jean-Louis Boulanger (UT Compiègne, France) V and V dans le cadre des systèmes certifiables
Les méthodes formelles ont été mises en oeuvre avec succés dans le cadre de la
réalisation de système complexe ayant un impact sur la vie des personnes. De
tel systèmes sont dit "critique" et "sûr de fonctionnement". Pour chaque
domaine (ferroviaire, nucléaire, aéronautique, ...), il existe des référentiels
définissant les processus a mettre en oeuvre. Dans certain cas, il existe
parmis ces processus des activités obligatoires liées à la certification du
système.



Dans le cadre de cette présentation, nous rappelerons les exigences associées
aux systèmes certifiables. Nous ferons le point de ce qui a été fait et nous
montrerons les contraintes qui restent a prendre en compte et les évolutions en
cours.



Mot-clés : méthode formelle, SAET-METEOR, Système certifiable, système critique,
UML, ...
2007-11-29Thomas Gazagnaire (IRISA, Rennes, France) _HMSC Causaux_
Les formalismes permettant de décrire l'interaction entre plusieurs entités distribuées et concurrentes ne manquent pas : automates asynchrones, automates communicants, réseaux de Petri, HMSC ... Ces formalismes sont tous très expressifs, et par conséquence il est souvent impossible de vérifier certaines propriétés basiques sur ces modèles. Ainsi, en général, on essaye de limiter la puissance d'expression de ces formalismes (en ajoutant, par exemple, des contraintes syntaxiques ou des bornes sur les canaux de communication) afin de rendre certains problèmes décidables.

Dans cet exposé nous introduisons une extension des HMSC appelée HMSC causaux, qui ajoute aux HMSC classiques la possibilité de commuter sur chaque processus certains évènements. Cette extension permet de modéliser des langages de MSC non finiment engendrés et non existentiellement bornés. Nous introduisons ensuite deux sous-classes syntaxiques de cette extension, les HMSC causaux réguliers et les HMSC causaux globalement-coopératifs, qui étendent strictement les classes du même nom pour les HMSC. Nous montrons que pour la première de ces classes, la régularité du langage des entrelacement est assurée, et pour la seconde l'inclusion et la vacuité de l'intersection est décidable.
2007-10-25Florian Horn (LIAFA, Paris) Des Fruits Aléatoires sur l'Arbre de Zielonka
Les jeux stochastiques constituent un modèle naturel
pour la synthèse de contrôleurs en milieux ouvert,
lorsque certaines actions peuvent être considérées
comme aléatoires. Les jeux $omega$-réguliers, dont
les parties sont de longueur infinie, peuvent ainsi
représenter des systèmes réactifs qui doivent réagir
correctement à un flux continuel d'évènements. Une
ressource critique pour ce genre d'applications est la
mémoire utilisée lors de l'implémentation effective du
contrôleur. Pour chaque condition de Muller, on peut
déduire de l'"arbre de Zielonka" la quantité de
mémoire nécessaire et suffisante pour définir des
stratégies gagnantes.

Dans cet exposé, je montrerai comment l'utilisation de
stratégies randomisées permet de gagner "presque
sûrement" à moindre coût dans chaque arène. Dans ce
contexte également, c'est à partir de l'étude de
l'"arbre de Zielonka" que l'on définit une meilleure
borne supérieure. De plus, pour chaque condition, il
existe certaines arènes (de taille exponentielle) pour
lesquelles des stratégies utilisant moins de mémoire
sont presque sûrement perdantes.
2007-10-11Holger Hermanns (Saarland University (Saarbruecken, Germany)) The quest for quantifiable quality
_Model checking_ is one of the main strategies to guarantee correctness
of system design. In the era of modern, power-aware, wireless and
distributed systems, correctness guarantees for such systems must become _quantifiable_. Instead of guaranteeing that a system is performing the
expected tasks, we are ultimately interested in guaranteeing that the
system performs its task within a given _time_ bound and with (energy)
_costs_ within a given limit. Or better: that the _probability_ thereof
is above a given threshold. In this talk I paint the landscape of
behavioural models for probability, time, and cost, and discuss
foundational and practical aspects of model checking such systems.
A more detailled look into our own work on continuous-time,
concurrent Markov models concludes the presentation.
2007-09-27Igor Walukiewicz (LaBRI, Bordeaux, France) A lower bound on web-services composition
In this talk a web service is modeled as a finite state machine. A composition
problem for web services is to decide if a given web service can be
constructed from a given set of web services; where the construction
is understood as a simulation of the specification by a fully asynchronous
product of the given services. We present an EXPTIME-lower bound for this problem,
thus matching the known upper bound. Our result
also applies to richer models of web services, such as the Roman
model.


Archives des années précédentes



Responsable

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