Groupe de travail

Modélisation et Vérification


To: mvtsi-gt@labri.fr
Cc:
Subject: [GT MVTsi -- Séminaire]

Chers collègues,
Nous n'aurons pas de séminaire jeudi prochain (2009-09-17).
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
2009-06-18Denis Lugiez (LIFM, Marseille) Edition Collaborative d'arbres XML
L'edition collaborative consiste à travailler sur un document commun de
manière distribuée et concurrente. Un problème essentiel est d'assurer la
cohérence du processus, car des opérations concurrentes peuvent etre
conflictuelles (ajouter ou supprimer une lettre à la meme position). De
nombreux systèmes reposent sur une centralisation implicite (par des
time-stamps par exemple) ou explicite (existence d'un site maitre comme avec
svn). L'approche Pair à Pair ne permet pas cette centralisation, et à tout
moment de nouveaux sites peuvent rejoindre le processus d'édition. Dans ce
cadre l'approche optimiste considère que toutes les opérations doivent etre
prises en compte, et utilise une approche transformationnelle pour intégrer
les opérations concurrentes: au lieu d'effectuer l'opération o2 concurrente à
o1, on effectue une opération modifiée IT(o1,o2). Quand l'opérateur de
transformation IT satisfait deux propriétés TP1 et TP2, il existe un
algorithme qui assure la convergence du processus (chaque site a la meme
copie du document à la fin du processus). Pour le cas des mots aucun des
jeux
d'opérations et des transformations proposées ne satisfont ces propriétés et
des contre-exemples montrent qu'ils n'assurent pas la convergence (cf thèse
d'A. Imine). Dans cet exposé nous nous intéressons à l'édition des arbres
étiquetés non-ordonnés avec des opérations d'ajout, suppression ou
réétiquetage. Le premier résultat est de montrer qu'il n'existe pas de
transformation satisfaisant TP1 et TP2 dans ce cadre. Le deuxième résultat
consiste à étendre la structure de données par des informations fournies
naturellement par le processus d'édition qui garantissent l'unicité des
étiquettes et de montrer que les propriétés TP1 et TP2 sont satisfaites ce
qui autorise l'edition collaborative sur cette structure. Finalement, nous
montrons comment garder ces propriétés en ajoutant une opération de
déplacement de sous-arbres à condition de modifier la structure de donnée en
ajoutant une mémoire. Nous terminerons en discutant le cas des arbres
ordonnés et le problème du undo (annulation d'une opération).

Travail en commun avec Stéphane Martin.
2009-06-04André Arnold () Contrôleurs non déterministes de processus non déterministes
Arnold, Vincent, Walukiewicz en 2003, puis Briand en 2006, on tracé une frontière entre les cas où la synthèse (centralisée ou décentralisée) de contrôleurs déterministes de processus déterministes est effective et ceux où elle est indécidable, lorsque les contrôleurs et le système contrôlé sont soumis à des contraintes d'inobservabilité et d'indiscernabilité exprimables dans un mu-calcul modal étendu.

En 2008 Arnold et Walukiewicz ont étendu ces résultats au cas où les contrôleurs et les processus ne sont pas nécessairement déterministes.

Ce sont ces extensions qui seront présentées.
2009-05-28Nathalie Bertrand (IRISA, Rennes, France) When are Timed Automata Determinizable?
We describe an abstract procedure which, given a timed automaton, produces a language-equivalent deterministic infinite timed tree. Under a certain boundedness condition, the infinite timed tree can be reduced into a classical deterministic timed automaton. The boundedness condition we exhibit is satisfied by several subclasses of timed automata, some of them were known to be determinizable (event-clock timed automata, automata with integer resets), but some others were not. We prove for instance that strongly non-Zeno timed automata can be determinized. As a corollary of those constructions, we get for those classes the decidability of the universality and of the inclusion problems, and compute their complexities (the inclusion problem is for instance EXPSPACE-complete for strongly non-Zeno timed automata).

This is a joint work with C. Baier, P. Bouyer and T. Brihaye.
2009-05-14Pierre Ganty (UCLA, Los Angeles, California) What's decidable for Asynchronous Programs ?
An asynchronous or "event-driven'' program is one that contains
procedure calls which are not directly executed from the call site,
but stored and executed later by an external scheduler.
By providing a low-overhead way to manage concurrent interactions,
asynchronous programs form the core of many server programs, embedded
systems, and popular programming styles for the web (Ajax).
Unfortunately, such programs can be hard to write and maintain as
sequential control flow needs to be split into several disjoint
handlers.
They are a challenge for static analysis tools as they are infinite
state: both the program stack and the number of outstanding
asynchronous requests may be unbounded.
We show that safety and liveness properties can be checked effectively
for the class of Boolean asynchronous programs, thus enabling
automatic static techniques to check for correctness or for errors.
2009-05-07Alain Finkel (LSV, Cachan, France) Well Structured Transition Systems everywhere and everytime !
The theory of Well Structured Transition Systems provides the good structure for computing a finite basis of the set of predecessors of the upward closure of a finite set of states. We address here the dual problem which is to compute a finite representation of the set of successors of the downward closure of a finite set of states (called the cover). This last problem is, a priori, more difficult because in general, the cover has no finite basis.
It is possible to complete any well-ordered set to obtain a cpo in which every downward closed set has a finite representation.
We then define the framework of Complete Well Structured Transition Systems and we propose a simple and a conceptual procedure for computing the covering set and the covering graph. This procedure terminates more often than the generalized Karp-Miller tree procedure when applied on extended Petri nets and lossy channel systems.
2009-04-30Stéphane Gaubert (INRIA and CMAP, Ecole Polytechnique) Algorithmes de théorie des jeux en analyse statique de programme
Nous ferons un tour d’horizon de résultats portant sur la
correspondance entre les équations de point fixe rencontrées en
analyse statique de programme par interprétation abstraite et celles
qui apparaissent dans l’approche par programmation dynamique des
jeux répétés à somme nulle. Cette correspondance permet en
particulier d’appliquer des algorithmes de type itération sur les
politiques afin de déterminer des invariants de nature numérique sur
le programme analysé (par exemple des invariants polyédraux).
Cependant, deux difficultés apparaissent. La première, très
inhabituelle, est que les jeux considérés peuvent avoir un taux
d’escompte négatif (l’ensemble des points fixes n’est plus alors
nécessairement connexe). Une seconde difficulté est que l’algorithme
d’itération sur les politiques le plus simple peut terminer avec un
point fixe non minimal, alors que c’est le point fixe minimal qui
fournit le meilleur invariant. Nous montrons cependant comment
utiliser des techniques de théorie de Perron-Frobenius non-linéaire
(rayons spectraux, calcul semi-différentiel) pour obtenir toujours
le plus petit point fixe, à condition que le taux d’escompte ne soit
pas négatif. Ces résultats sont issus d’une série de travaux avec
Éric Goubault, Matthieu Martel, Sylvie Putot, Alexandru Costan,
Ankur Taly, et Assale Adjé.
2009-04-23Sylvain Sené (LIRIS, Villeurbanne) Robustesse environnementale dans les réseaux d'automates à seuil : théorie et application en biologie.
Nous allons nous intéresser à l'influence des conditions de bords dans les réseaux d'automates booléens à seuil, objets mathématiques pertinents pour la modélisation des réseaux de régulation biologique. L'objectif est de montrer que les bords (qui peuvent représenter des potentiels électriques externes dans les réseaux de neurones et des flux d'hormones ou encore des micro-ARN dans les réseaux de régulation génétique) sont des éléments qui peuvent changer radicalement le comportement dynamique de tels réseaux, aussi bien dans le cas de réseaux théoriques tels que les automates cellulaires que dans celui des réseaux biologiques réels. La démarche scientifique proposée est de se focaliser dans un premier temps sur des réseaux dits "parfaits", énormément contraints sur la nature des interactions et la topologie de manière à obtenir des résultats théoriques sur Z^d. Ensuite, en relâchant progressivement les contraintes, nous mettrons en évidence, par simulation, des domaines d'influence des conditions de bord pour des réseaux plus complexes sur Z2. Enfin, pour faire un pas de plus en direction de la biologie, nous verrons que les conditions de bord jouent un rôle dans les réseaux réels. Nous présenterons alors une méthode générique d'étude de la robustesse environnementale des systèmes dynamiques réels (basée sur la notion de bassin d'attraction). Nous terminerons en présentant les résultats que cette méthode permet d'obtenir, dans le contexte des réseaux de régulation génétique, à propos de la morphogenèse florale de la plante Arabidopsis thaliana.
2009-04-02David Teller-Rajchenbach (université d'Orléans) Extrapol, des systèmes de types dépendants à la sécurité système
Dans le domaine de la sécurité, l'un des problèmes récurrents est celui
de déterminer quels effets l'exécution d'un programme peut avoir sur le
système qui l'héberge. Ces effets peuvent prendre la forme de
modification de fichiers, de communication avec des processus,
d'installation de services web... Dans d'autres cas, c'est
l'installation d'un programme ou d'une bibliothèque qui pourra donner à
d'autres programmes des points d'entrée pour avoir ce même genre
d'effets, de manière potentiellement accidentelle et potentiellement
malicieuse.

Le plus fréquemment, pour détecter les effets d'un programme ou les
points d'entrée d'une bibliothèque, l'administrateur d'un système a le
choix entre des outils dynamiques (bacs à sable) et des outils
post-mortem (analyse de trace) -- mais pas réellement d'outils d'analyse
statique.

Au cours de notre exposé, nous présenterons une technique d'analyse
statique pour les propriétés de sécurité de code source écrit en langage
C. Nous partirons du modèle de sécurité SELinux, tel qu'intégré à de
nombreuses distributions de Linux, et nous avancerons progressivement
jusqu'à une notion de types avec effets et de types dépendants. La
technique a été implantée en OCaml, sous la forme d'un outil de
diagnostic automatique, Extrapol.
2009-03-19Alain Griffault (LaBRI, Bordeaux, France) AltaRica : passé, présent et futur.
AltaRica est un formalisme qui a été défini pour la description fonctionnelle
et dysfonctionnelle des systèmes industriels critiques. Depuis la première
version du langage en 2000, différentes variantes et outils associés ont été
proposés. Aujourd'hui, ces outils sont réellement utilisés de façon
productive dans certaines entreprises.
Dans la première partie de l'exposé, je présenterai le formalisme initial et
sa sémantique. Je donnerais ensuite les diverses évolutions et les raisons
pour lesquelles elles ont été introduites.
La dernière partie de l'exposé listera des travaux futurs possibles dans le
cadre "AltaRica, un formalisme d'aide à la conception sûre de systèmes
critiques".
2009-03-12Paul Gastin (LSV, Cachan, France) How to get decidability of distributed synthesis ?
The distributed synthesis problem is to come up with a local strategy for each process such that the resulting behaviours of the system meet a given specification.

Our general aim is to define natural conditions under which synthesis or control are decidable for distributed systems. It is known that these problems are undecidable for most synchronous systems. So in this work we study asynchronous systems which communicate through signals -- actions that are immediately received by the target process. Another main cause of undecidability comes from the specifications. Here, we consider emph{external} specifications over emph{partial orders}. External means that specifications only relate input and output actions from and to the environment and not internal signals exchanged by processes. We also ask for some natural closure properties of the specification. We obtain decidability for the subclass of networks where communication happens through a strongly connected graph. We believe that this framework for distributed synthesis yields decidability results for many more architectures.
2009-03-05Stéphane Demri (LSV, Cachan, France) Modal Logics with Presburger constraints
In this talk, we present an extended modal logic EML with regularity constraints and
full Presburger constraints on the number of children that generalize graded modalities,
also known as number restrictions in description logics.
We show that the satisfiability problem for EML can be solved with polynomial space.
This extends a well-known and non-trivial PSPACE upper bound for graded modal logic.
Furthermore, we provide a detailed comparison with logics that contain
Presburger constraints and that are dedicated to query XML documents. As an
application, we provide a reduction from Sheaves logic SL into EML,
which allows to improve the best known upper bound for SL satisfiability.

This is a joint work with Denis Lugiez (LIF, Marseille, France).
2009-02-12Omer NGUENA (LaBRI, Bordeaux, France) Spécification et Contrôle des Systèmes temps-réel faibles
Nous introduisons la Logique $WT_mu$ pour décrire les propriétés des systèmes temps-réel faibles et nous synthétisons les contrôleurs des ces systèmes lorsque les propriétés sont écrites en $WT_mu$.
2009-01-23Mikolaj Bojanczyk (Institute of Informatics, Warsaw University) Max-regular languages
A new class of languages of infinite words is introduced, called the
max-regular languages, extending the class of omega-regular languages.
The class has two equivalent descriptions: in terms of automata (a
type of deterministic counter automaton), and in terms of logic (weak
monadic second-order logic with a bounding quantifier). Effective
translations between the logic and automata are given.
2009-01-08Pierre Cyril Heam (LIFC, Université de Franche0Compté) Génération Automatique d'Approximations Régulières
Etant donnés deux langages réguliers d'arbres I et B, et un système de
réécriture R, on ne peut pas décider si R*(I) et B ont une intersection
vide, même pour des systèmes de réécritures simples. Une approche pour
résoudre ce problème consiste alors à utiliser des approximations de
R*(I). Nous montrerons dans cet exposé comment une technique manuelle
d'approximations introduite par Th. Genet en 98 peut être automatisée,
notamment pour la vérification de protocoles cryptographiques.

2008-12-18Alexander Heussner (LaBRI, Bordeaux, France) CEGAR for Communicating Fifo Systems
The automatic verification of asynchronous communication
protocols demands for methods that are able to process
infinite state spaces and emergent behaviour. Communicating
fifo systems are a standard model for distributed
processes which are represented by a set of finite
automata that exchange messages over a network of reliable,
unbounded fifo channels.

We utilize the counterexample-guided abstraction
refinement technique (CEGAR) for the automatic
verification of communicating fifo systems regarding
safety properties. This is accomplished with the help of
predicate abstraction and a predicate refinement strategy
relying on the computation of path
invariants based on an additional extrapolation operator
for recognizable languages.

The presentation of the verification algorithm is completed
by a brief presentation of a prototypical implementation.
2008-12-11Pawel Parys (Warsaw University, Poland) XPath evaluation in linear time
We consider a fragment of XPath where attribute values can only be tested for equality. We show that for any fixed unary query in this fragment, the set of nodes that satisfy the query can be calculated in time linear in the document size.
2008-12-04Ahmed Bouajjani (LIAFA, Paris) Analyzing Asynchronous Programs with Preemption
Multiset pushdown systems have been introduced by Sen and Viswanathan as
an adequate model for asynchronous programs where some procedure calls
can be stored as tasks to be processed later. The model is a pushdown
system supplied with a multiset of pending tasks. Tasks may be added to
the multiset at each transition, whereas a task is taken from the
multiset only when the stack is empty. In this paper, we consider an
extension of these models where tasks may be of different priority
level, and can be preempted at any point of their execution by tasks of
higher priority. We investigate the control point reachability problem
for these models. Our main result is that this problem is decidable by
reduction to the reachability problem for a decidable class of Petri
nets with inhibitor arcs. We also identify two subclasses of these
models for which the control point reachability problem is reducible
respectively to the reachability problem and to the coverability problem
for Petri nets (without inhibitor arcs).

This is a joint work with Mohamed Faouzi Atig and Tayssir Touili.
2008-11-27Tayssir Touili (LIAFA, Paris) On the Reachability Analysis of Acyclic Networks of Pushdown Systems
We address the reachability problem in acyclic networks of pushdown systems. We consider
communication based either on shared memory or on message passing through unbounded
lossy channels. We prove mainly that the reachability problem between recognizable sets of
configurations (i.e., definable by a finite union of products of finite-state automata) is decidable
for such networks, and that for lossy channel pushdown networks, the channel language is
effectively recognizable. This fact holds although the set of reachable configurations
(including stack contents) for a network of depth (at least) 2 is not rational in general (i.e., not
definable by a multi-tape finite automaton). Moreover, we prove that for a network of depth 1,
the reachability set is rational and effectively constructible (under an additional condition on
the topology for lossy channel networks).

This is a joint work with Mohamed Faouzi Atig and Ahmed Bouajjani
2008-11-20Xavier ALLAMIGEON (EADS) Inferring Min and Max Invariants Using Max-plus Polyhedra
We introduce a new numerical abstract domain able to infer min and max invariants over
the program variables, based on max-plus polyhedra. Our abstraction is more precise than
octagons, and allows to express non-convex properties without any disjunctive
representations. We have defined sound abstract operators, evaluated their complexity,
and implemented them in a static analyzer. It is able to automatically compute precise
properties on numerical and memory manipulating programs such as algorithms on strings
and arrays.
2008-11-13Arnaud Sangnier (LSV, ENS-Cachan) Reversal-Bounded Counter Machines Revisited
We extend the class of reversal-bounded counter machines by authorizing a finite number of alternations between increasing and decreasing mode over a given bound. We prove that extended reversal-bounded counter machines also have effective semi-linear reachability sets and enjoy the same properties as the original reversal-bounded counter machines. We also prove that the property of being reversal-bounded is undecidable in general even when we fix the bound, whereas this problem becomes decidable when considering Vector Addition System with States.

This is a joint work with Alain Finkel.
2008-11-06Blaise Genest (IRISA, Rennes, France) Quasi-Static Scheduling of Communicating Tasks
Good scheduling policies for distributed embedded applications are required for meeting hard real time constraints and for optimizing the use of computational resources. We study the quasi-static scheduling problem in which (uncontrollable) control flow branchings can influence scheduling decisions at run time. Our abstracted task model consists of a network of sequential processes that communicate via point-to-point buffers. In each round, the task gets activated by a request from the environment. When the task has finished computing the required responses, it reaches a pre-determined configuration and is ready to receive a new request from the environment. For such systems, we prove that determining existence of quasi-static scheduling policies is undecidable. However, we show that the problem is decidable for the important sub-class of “data branching” systems in which control flow branchings are due exclusively to data-dependent internal choices made by the sequential components. This decidability result—which is non-trivial to establish—exploits ideas derived from the Karp and Miller coverability tree as well as the existential boundedness notion of languages of message sequence charts.


This is a joint work with philippe Darondeau, P.S. Thiagarajan and Shaofa Yang.
2008-10-16Serge Haddad (LSV, Cachan, France) Logiques pour le model checking des chaînes de Markov à temps continu
Markov chains are a well-known stochastic process that provide a
balance between being able to adequately model the system's behavior
and being able to afford the cost of the model solution.
Systems can be modelled directly as Markov chains, or with a higher-level
formalism for which Markov chains represent the underlying semantics.
Markov chains are widely used to study the performance of
computer and telecommunication systems.
The definition of stochastic temporal logics like Continuous Stochastic
Logic (CSL)
and its variant asCSL, and of their model-checking algorithms,
allows a unified approach
to the verification of systems, allowing the mix of performance evaluation and
probabilistic verification.


In this talk we present the stochastic logic CSLTA,
which is more expressive than
CSL and asCSL, and in which properties can be specified using automata
(more precisely, timed automata with a single clock).
The extension with respect to expressiveness allows the specification of
properties referring to the probability of a finite sequence of timed events.
A typical example is the responsiveness property
``with probability at least 0.75, a message sent at time 0 by a system A
will be received before time 5 by system B and the acknowledgment will be back at A before time 7'', a
property that cannot be expressed in either CSL or asCSL.
Furthermore, the choice of using automata rather than the
classical temporal operators
Next and Until should help in enlarging the accessibility of model checking to a larger
public.
We also present a model-checking algorithm for CSLTA.
2008-10-09Hélène Kirchner (INRIA Bordeaux - Sud-Ouest) A rewrite-based approach for security policies
We show how strategic rewriting and narrowing provide a foundational framework
for the compositional design, maintenance and verification of security policies.
Rewrite rules transform input terms representing policy requests into decision terms.
Strategies are used to explicitly control the rule application.
Parameterized queries are solved by narrowing.
Relying on the correspondences between the properties of the rewrite system and the policy it implements,
we are able to reuse existing proof techniques and analysis tools in the security policies context.


Joint work with Claude Kirchner and Anderson Santana de Oliveira
2008-09-25Jérôme Leroux (LaBRI, Bordeaux, France) An Easy Algorithm For The General Vector Addition System Reachability Problem
The reachability problem for Vector Addition Systems (VAS) or equivalently for Petri Nets is a central problem of net theory. The general problem is known decidable by algorithms exclusively based on the classical Kosaraju-Lambert-Mayr-Sacerdote-Tenney (KLMST) decomposition. This decomposition is difficult and it just has a non-primitive recursive upper-bound complexity. In this paper, we prove that if a final configuration is not reachable from an initial one, there exists a pair of Presburger formulas denoting an inductive separator proving this property. Since we can decide with any decision procedure for the Presburger arithmetic if pairs of Presburger formulas denote inductive separators, we deduce that there exist checkable certificates of non-reachability. In particular, there exists an easy algorithm for deciding the general VAS reachability problem based on two semi-algorithms. A first one that tries to prove the reachability by fairly enumerating finite sequence of actions and a second one that tries to prove the non-reachability by fairly enumerating pairs of Presburger formulas. Even if the KLMST decomposition is used for proving the termination, this algorithm is the very first one that can be implemented without using it.
2008-09-18(1) Jean-Christophe Filliâtre et (2) Sylvain Conchon (LRI, Université Paris Sud, France) (1) Utilisation de prouveurs SMT pour la preuve de programmes et (2) Vérification de propriétés de programmes avec Alt-Ergo
(1)
Cet exposé présente l'utilisation de prouveurs SMT pour la preuve de
programmes C et Java dans le cadre de la plateforme Why
(http://why.lri.fr/). En particulier, on justifie le choix d'une logique
du premier ordre polymorphe comme langage d'entrée pour utiliser les
différents prouveurs SMT, et on explique comment cette logique est
encodée lorsque le prouveur SMT ne l'implante pas nativement.
Cet exposé indique également quelles sont les théories pertinentes pour
la vérification de programmes, et comment leur absence dans certains
prouveurs SMT peut être contournée à l'aide de modèles axiomatiques.
Enfin, on explique comment les prouveurs SMT peuvent être utilisés
depuis l'assistant de preuve Coq, lorsque la preuve interactive devient
nécessaire.


(2)
Alt-Ergo est un démonstrateur automatique de théorèmes dédié à la
vérification de propriétés de programmes. Les formules logiques
envoyées à Alt-Ergo sont écrites dans la logique du 1er ordre
polymorphe multi-sortée de l'outil Why.

Dans cet exposé nous décrirons l'architecture d'Alt-Ergo. Elle est
composée d'un SAT-solver qui interagit avec un algorithme de
combinaison de procédures de décision et un mécanisme d'instanciation
pour traiter les formules quantifiées.

Le code d'Alt-Ergo est très court (environ 4000 lignes d'Ocaml) ce qui
en fait un bon candidat pour réaliser la preuve en Coq d'un
démonstrateur automatique. Alt-Ergo est disponible à
http://alt-ergo.lri.fr


Archives des années précédentes



Responsable

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