2005 - 2006

Groupe de travail

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

Le jeudi de 11h à 12h15
Salle 076, LaBRI, Rez-de-chaussée




Prévisions





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


8 juin 2006
Thierry Jéron (IRISA, Rennes)
Sélection de tests par analyse approchée

Dans cet exposé, nous nous inéressons au problème de la sélection de cas de tests pour tester la conformité des systèmes réactifs. Nous nous placons dans le cadre de la théorie du test proposée par Tretmans, où les systèmes sont modélisés par des systèmes de transition à entrée/sortie (IOLTS) et la relation de conformité qui définit les implémentations conformes par rapport à une spécification (ioco) est une inclusion partielle de comportements observables.

Nous considérons ici des systèmes à espace d'état infini représentés par des automates étendus (IOSTS) et le problème de sélection de tests pour un objectif de test décrit par un IOSTS avec états marqués. Le but de la sélection est de produire un cas de tests sous la forme d'un IOSTS qui permette de tester à la fois la non-conformité et la reconnaissance par l'objectif. Ceci se ramène à un problème de co-accessibilité d'états dans des IOSTS, indécidable dans ce modèle. Cependant, nous montrons qu'un calcul approché par interprétation abstraite permet de produire des cas de tests corrects. Nous étendons l'approche à des objectifs d'atteignabilité et de sûreté.

18 mai 2006
Richard Mayr (North Carolina State University, USA)
Verification Methods for Infinite-State Probabilistic Systems
Probabilistic systems can be used for modeling systems that exhibit uncertainty, such as communication protocols over unreliable channels, randomized distributed systems, or fault-tolerant systems. Finite-state models of such systems often use variants of probabilistic automata whose underlying semantics is defined in terms of homogeneous Markov chains. These have been studied extensively and many verification problems are easily computable for them. However, many techniques and results do not carry over to probabilistic systems with infinitely many states. Here we give an overview over recent emerging techniques in this area.

(1) Approximation algorithms compute numerical approximations, up-to arbitrary precision, of interesting system properties, like the probability of satisfying a requirements specification, or a performance parameter.

(2) Symbolic analysis techniques reduce the verification problem to known algebraic problems, e.g., systems of polynomial equations, which can be solved by techniques from computer algebra.

11 may 2006
Tayssir Touili (LIAFA, Paris)
Verifying Concurrent Message-Passing C Programs with Recursive Calls
We consider the model-checking problem for C programs with (1) data ranging over very large domains, (2) (recursive) procedure calls, and (3) concurrent parallel components that communicate via synchronizing actions. We model such programs using communicating pushdown systems, and reduce the reachability problem for this model to deciding the emptiness of the intersection of two context-free languages L1 and L2. We tackle this undecidable problem using a CounterExample Guided Abstraction Refinement (CEGAR) scheme. We implemented our technique in the model checker MAGIC and found a previously unknown bug in a version of a Windows NT Bluetooth driver. This is a joint work with S. Chaki, E. Clarke, N. Kidd, and T. Reps.
4 mai 2006
Hervé Marchand (IRISA, Rennes)
Motifs de surveillance pour diagnostic de systèmes à évènements discrets
Durant cet exposé nous nous intéressons au diagnostic dans les systèmes de transition finis. Nous proposons un modèle de motifs de surveillance correspondant à des propriétés d'atteignabilité. Ceci permet de généraliser les propriétés à diagnostiquer tout en les découplant de la description du système. Nous en déduisons des techniques de vérification de diagnosticabilité et de construction de diagnostiqueur fondées sur des opérations standards sur les systèmes de transitions. Nous montrons que ces techniques sont suffisamment générales pour exprimer et résoudre de manière unifiée une classe importante de problèmes de diagnostic considérés dans la littérature comme le diagnostic de pannes permanentes, de pannes multiples, de séquences de pannes, et certains problèmes de diagnostic de pannes intermittentes.
27 avril 2006
Hubert Garavel (INRIA Rhône-Alpes)
Validation d'architectures multiprocesseurs à l'aide les outils CADP
Dans cet exposé, nous présentons d'abord l'architecture logicielle et les principales fonctionnalités de la boîte à outils CADP (http://www.inrialpes.fr/vasy/cadp) dont une nouvelle version stable devrait apparaître dans les prochaines semaines. Nous présentons ensuite les principaux résultats de la collaboration entre Bull et l'INRIA pour améliorer la qualité et la productivité dans la conception d'architectures multiprocesseurs complexes. Nous illustrons les résultats obtenus avec CADP sur trois architectures de Bull (PowerScale, PolyKid et Fame).
13 avril 2006
Nicolas Baudru (LIF, Marseille)
Unfolding Synthesis of Asynchronous Automata
Zielonka's theorem shows that each regular set of Mazurkiewicz traces can be implemented as a system of synchronized processes provided with some distributed control structure called an asynchronous automaton. This paper gives a new algorithm for the synthesis of a non-deterministic asynchronous automaton from a regular Mazurkiewicz trace language. Our approach is based on a simple unfolding procedure that improves the complexity of Zielonka's and Pighizzini's techniques: Our construction is polynomial in terms of the number of states but still double-exponential in the size of the alphabet.
6 avril 2006
Samy Abbes (LIAFA, Paris)
Concurrent Probabilistic Models

Large distributed systems are numerous in information technology. For such systems, only local states can be considered, not global ones (what would it mean considering the state of the Web?); similarly, events can only be ordered locally in time, not globally; last, there are plenty of subsystems that progress independently without interacting for some period of time (and even sometimes for ever). Probabilistic models that take these features into account have been only recently developed, independently by Varacca and Winskel, and by Abbes and Benveniste.

The talk focuses on Markov nets, an extension of Markov chains to distributed and concurrent systems. Our starting point are (1-safe) Petri nets with true-concurrency semantics; this means that executions of the net are modeled by traces, not firing sequence; a trace is the equivalence class of firing sequences modulo the exchange of concurrent consecutive events (transitions). This way, irrelevant interleavings are not considered and states become really local (the marking graph is never considered).

We show how to construct probabilities on the space of all maximal traces of a net. A particular construction yields the Markov nets. Markov nets satisfy a strong Markov property, plus a new property stating that concurrent subsystems are probabilistically independent (a property not satisfied by previous stochastic Petri net models). They also satisfy a new local renewal theory and a new law of large numbers. This analysis is interesting for concurrency theory in general, as it points out the very nature of choice and local state in nondeterministic systems. This study was originally motivated by distributed fault management and alarm correlation in telecom networks.

Joint work with Albert Benveniste (INRIA/IRISA)

30 mars 2006
Jerome Feret (ENS, Paris)
Analyse des systemes mobiles par interpretation abstraite

Un systeme mobile est un ensemble de composants qui peuvent interagir entre eux, tout en modifiant dynamiquement le systeme lui-meme. Ces interactions controlent ainsi la creation et la destruction des liaisons entre les composants, mais aussi la creation dynamique de nouveaux composants au sein du systeme. La taille d'un tel systeme varie au cours du temps, elle n'est pas bornee en general. Un systeme mobile peut representer des reseaux de telecommunication, des systemes reconfigurables, des applications client-serveur sur la toile, des protocoles cryptographiques, ou des systemes biologiques. Plusieurs modeles sont disponibles selon le domaine d'application et la granularite du niveau d'observation.

Nous proposons un cadre de travail unifiant pour decouvrir et prouver statiquement (avant leur execution) et automatiquement les proprietes des systemes mobiles. Nous proposons un meta-langage dans lequel nous encodons les modeles les plus couramment utilises dans la littrature (le pi-calcul, le calcul des ambients, le join-calcul, le spi-calcul, les Bio-ambients, etc). Pour chaque modele encode, le meta-langage calcule une semantique enrichie dans laquelle a la fois les composants et les objets qu'ils manipulent (addresses memoires, noms de canaux, clefs secretes ou partagees, etc) sont identifies par l'historique de leur creation. Ainsi, nous n'utilisons pas de relation de congruence (ni de renommage), ce qui rend l'analyse plus facile.

Le cadre general de l'Interprtation Abstraite nous permet ensuite de deriver des semantiques abstraites, qui sont decidables, correctes, et approchees. Dans cette these, nous donnons trois analyses generiques que nous instancions selon le compromis desire entre le temps de calcul et la precision de l'analyse. La premiere analyse se concentre sur les proprietes dynamiques du systeme. Elle infere des relations entre les historiques des objets qui sont manipules par les composants du systeme. Cette analyse distingue les instances recursives d'un meme objet, et ce, meme lorsque le nombre de ces instances n'est pas borne. A titre d'exemple, cette analyse prouve dans le cas d'une application client-serveur a nombre illimit de clients, que les donnees de chaque client ne sont pas communiquees aux autres clients. La deuxime analyse se concentre sur des proprites de concurrence. Cette analyse compte le nombre de composants du systeme. Elle permet de detecter que certains composants ne peuvent pas interagir, car ils ne coexistent jamais. Elle peut aussi garantir a un systeme qu'il n'epuisera pas les ressources physiques disponibles. Une troisieme analyse mele concurrence et dynamicite. Elle regroupe les composants d'un systeme en differentes unites de calcul, puis abstrait le nombre d'instances de composants au sein de chaque unite de calcul. Nous prouvons, par exemple, l'absence de conflits en ecriture dans une memoire partagee avec allocation dynamique.

23 mars 2006
Guillaume Feuillade (IRISA, Rennes)
Spécification logique de réseaux de Petri

Les objets concurrents présentent généralement des avantages pratiques sur les objets séquentiels : leur mise en oeuvre sur des architectures distribuées est plus aisée, il permettent de meilleures performances, etc. De fait, la construction automatique de modèles concurrents est un enjeu. Le sujet de cet exposé est l'étude des problèmes de synthèse de réseaux de Petri à partir de spécifications en logique du temps arborescent.

Les méthodes de synthèse à partir de spécifications logiques s'appuient généralement sur des automates de mots ou d'arbres pour générer des objets séquentiels. Obtenir un objet concurrent dans un second temps n'est pas toujours possible : en effet, le modèle séquentiel synthétisé lors de la première étape ne possède pas nécessairement les propriétés requises pour être distribuable. Par conséquent, les algorithmes existants ne s'appliquent pas dans notre cadre de synthèse d'objets concurrents ; la décidabilité du problème de synthèse est alors une question ouverte.

Sans intention de proposer un nouveau formalisme de spécification, nous investiguons la synthèse de réseaux de Petri à partir de spécifications en logique temporelle, et plus généralement celui de la satisfiabilité d'une formule sur la classe des réseaux de Petri. Nous prenons comme point de départ la plus expressive des logiques du temps arborescent : le Mu-Calcul. Le fil conducteur est la recherche de la frontière de décidabilité pour le problème de satifiabilité d'une formule sur la classe des réseaux de Petri ; nous proposons des restrictions successives de la logique pour approcher cette frontière.

Nous montrons qu'il est nécessaire de restreindre très fortement la logique pour rendre la synthèse décidable, et que des logiques pourtant faibles permettent d'obtenir l'expressivité des machines à compteurs lorsque ces logiques sont interprétées sur la classe des réseaux de Petri.

16 mars 2006
Jerome Leroux (LaBRI, Bordeaux)
Regular Acceleration for Number Decision Diagrams
The verification of an infinite state system often reduce to the computation of the reflexive and transitive closure of some binary relations over infinite set of states. Sébastien Bardin and Alain Finkel shown in 2004 that up to our knowledge, all the algorithms computing exactly such a reflexive and transitive closure, compute in fact a richer structure, called acceleration, as an intermediate step. In this paper, we prove that if the acceleration of a binary relation can be represented by a Number Decision Diagram (an automata-based symbolic representation for manipulating infinite sets of integer vectors), then it is effectively computable.
9 mars 2006
Jan Strejcek (Labri, Bordeaux)
On state-extensions of Process Rewrite Systems
Process rewrite systems (PRS) is one of the most successful formalisms for description of infinite-state systems. Three extensions of PRS formalism based on addition of finite-state control unit have been studied so far, namely: state extension, weak state extension, and extension with finite constraint system. We present an expressiveness hierarchy of all (extended as well as unextended) PRS classes and show that the hierarchy is strict with respect to strong bisimulation. We also present some (un)decidability results, for example:
  • reachability is decidable for weakly extended PRS
  • strong bisimulation between weakly extended PRS and finite-state systems is decidable
  • model checking of weakly extended PRS against Lamport logic (LTL restricted to operators always and eventually) is decidable
  • EF logic is decidable for weakly extended PAD (generalization of pushdown processes and BPP)
  • weak bisimulation is undecidable for all extensions of BPP and BPA
23 février 2006
Loïc Hélouët (IRISA, Rennes)
Jeux et scénarios pour la découverte de canaux cachés dans les systèmes distribués.
Les canaux cachés sont des fuites d'informations non prévues dans un système, qui détournent généralement des ressources pour transférer secrètement un message. Ces canaux cachés sont une menace pour la sécurité, les performances, mais aussi la rentabilité d'un système.

Tous les standards en matière de sécurité recommandent d'appliquer des audits aux systèmes pour identifier ces canaux cachés à l'aide de méthodes "reproductibles". De nombreuses méthodes formelles s'appuyant d'une part sur un modèle des systèmes étudiés, et d'autre part sur un modèle de sécurité Bell & La Padulla ont été proposées. Le modèle de Bell & La Padulla indique quels utilisateurs sont autorisés a communiquer entre eux, et les approches basées sur ce modèle vérifient généralement qu'il n'existe pas de flots d'information (par exemple en utilisant une ressource partagée) entre deux utilisateurs qui ne sont pas autorisés à échanger de l'information.

Nous proposons une méthode pour détecter des canx cachés à partir d'un modèle de protocole défini par des scénarios. L'approche que nous proposons rompt avec la vision traditionelle Bell-La PAdulla, en supposant qu'un canal caché peut également apparaître entre deux utilisateurs qui sont autorisés à communiquer si la manière dont le protocole est utilisé est un phénomène observable.

Dans un premier temps, nous modélisons un canal caché comme un jeu, dans lequel une paire d'utilisateurs malicieux {S,R} cherche à transférer de l'information, tandis que le reste du protocole essaie de l'en empêcher. Les messages transférés sont codés par des choix de comportements à des instants précis, et décodés par des transducteurs dont le vocabulaire d'entrée est une observation du système. Nous montrons que si {S,R} possède une strategie gagnante dans ce jeu, et qu'il existe un décodeur pour le message transféré, alors il existe un canal caché dans le protocole modélisé.

9 février 2006
Laurent Van Begin (LIAFA, Paris)
A Complete Abstract Interpretation Framework for Coverability Properties of WSTS.
We present an abstract interpretation based approach to solve the coverability problem of well-structured transition systems. Our approach distinguishes from other attempts in that (1) we solve this problem for the whole class of well-structured transition systems using a forward algorithm. So, our algorithm has to deal with possibly infinite downward closed sets. (2) Whereas other approaches have a non generic representation for downward closed sets of states, which turns out to be hard to devise in practice, we introduce a generic representation requiring no additional effort of implementation.
2 février 2006
David Janin (LaBRI, Bordeaux)
Synthèse de programmes distribués dans les architectures synchrones zéro-délais.
Dans cet exposé, je présenterais le problème de la synthèse de programmes distribués sur des architectures synchrones, sans délais et avec cycles.

Aprés un examen détaillé de la sémantique à donner à ces architectures (la présence de cycles sans délais impliquant, a priori, la résolution d'un système d'équations de points-fixes), je montrerais comment ce problème peut se coder en un problème de résolution de jeux distribués et, ainsi, être résolues par des méthodes connues (cas des architectures hiérarchique).

Cette présentation s'appuie sur un travail effectué au LaBRI en collaboration avec Julien Bernet et Igor Walukiewicz.

26 janvier 2006
Patricia Bouyer (LSV, Cachan)
Jeux temporisés optimaux
Les jeux temporisés à coûts étendent les jeux temporisés classiques avec des coûts à la fois dans les états et sur les transitions. En 2004, ces jeux ont été étudiés indépendemment dans [ABM04] et [BCFL04], et il a été en particulier montré que le coût optimal pour gagner de tels jeux est calculable sous certaines conditions de coût strictement non-zenon. Plus récemment (dans [BBR05] puis dans [BBM06]), il a été montré que le coût optimal n'est en général pas calculable sans l'hypothèse sur le coût mentionnée ci-dessus. Dans cet exposé, nous présenterons le modèle de jeu que l'on considère et nous présenterons quelques-uns des résultats qui ont été obtenus, notamment la (non-)calculabilité du coût optimal, les propriétés des stratégies gagnantes optimales, et des bornes de complexité.

[ABM04] Rajeev Alur, Mikhail Bernadsky, and P. Madhusudan. Optimal reachability in weighted timed games. In Proc. ICALP'04, vol. 3142 of LNCS, p. 122-133.

[BBM06] Patricia Bouyer, Thomas Brihaye, and Nicolas Markey. Improved undecidability results on weighted timed automata. To appear in IPL.

[BBR05] Thomas Brihaye, Véronique Bruyère, and Jean-François Raskin. On optimal timed strategies. In Proc. FORMATS'05, vol. 3821 of LNCS, p. 49-64.

[BCFL04] Patricia Bouyer, Franck Cassez, Emmanuel Fleury, and Kim G. Larsen. Optimal strategies in priced timed game automata. In Proc. FSTTCS'04, vol. 3328 of LNCS, p. 148-160.

19 janvier 2006
Thomas Brihaye (Univ. Mons-Hainaut)
Vérification d'automates hybrides o-minimaux
Les automates hybrides o-minimaux ont été introduits par G.Lafferriere, G.J.Pappas and S.Sastry dans [LPS00]. Ces automates hybrides jouissent d'une dynamique continue particulièrement riche et admettent néanmoins une bisimulation finie ([LPS00]). Dans cet exposé, nous commencerons par rappeler la notion d'automate hybride o-minimal. Nous donnerons ensuite une preuve de l'existence d'une bisimulation finie pour les automates hybrides o-minimaux. Pour cette preuve nous nous baserons sur la technique d'encodage des trajectoires par des mots introduite dans [BMRT04] (voir aussi [BM04,Bri]). Nous nous interesserons finalement au contrôle de ces automates. Nous verrons que la technique d'encodage des trajectoires par des mots est parfaitement adaptée à l'étude de ce problème (voir [BBC05]).

[BBC05] Patricia Bouyer, Thomas Brihaye, Fabrice Chevalier, Control in o-minimal hybrid systems, Research Report LSV-05-15, Laboratoire Spécification et Vérification, ENS Cachan, France, August 2005, 24 pages.

[BM04] Thomas Brihaye, Christian Michaux, On the expressiveness and decidability of o-minimal hybrid systems, Journal of Complexity, 21(4), 447-478, 2005.

[BMRT04] Thomas Brihaye, Christian Michaux, Cédric Rivière, Christophe Troestler, On O-Minimal Hybrid Systems, HSCC'04, LNCS 2993, Springer, 219-233, 2004.

[Bri] Thomas Brihaye, Words and Bisimulation of Dynamical Systems, to appear in Journal of Automata, Languages and Combinatorics, 23 pages, 2005.

[LPS00] Gerardo Lafferriere, George J. Pappas, Shankar Sastry, O-Minimal Hybrid Systems, Mathematics of Control, Signals, and Systems, 13(1), 1-21, 2000.

5 janvier 2006
Guillaume Gardey (LaBRI)
Contribution à la vérification et au contrôle des systèmes temps réel -- Applications aux réseaux de Petri temporels et aux automates temporisés

Dans cette thèse, nous proposons une approche pour la vérification et le contrôle de systèmes temps réel modélisés par des réseaux de Petri temporels ou des automates temporisés.

Notre approche se place dans le cadre du model-checking. Étant donnée une propriété exprimée dans un certain formalisme (états du modèle, logique temporelle , ...), sa vérification se fait en explorant tout ou partie de l'espace d'états du système modélisé. Nous proposons ainsi une méthode de calcul efficace de l'espace d'états d'un réseau de Petri temporel, méthode que nous étendons alors pour effectuer la vérification de propriétés quantitatives ie intégrant explicitement des contraintes temporelles. D'autres méthodes alternatives sont également proposées pour la vérification en utilisant notamment une traduction d'un réseau de Petri temporel borné en un automate temporisé temporellement bisimilaire.

Dans un second temps, la réponse au problème du model-checking n'étant pas toujours suffisante pour le concepteur d'un système, nous proposons d'étudier les problèmes de la synthèse de contrôleur assurant une propriété donnée. Dans le cas des réseaux de Petri temporels le contrôle de propriétés de sûreté exprimées sur ses marquages est étudiée alors que pour les automates temporisés nous nous intéressons au contrôle de propriétés plus complexes de non-interférence permettant de modéliser des problèmes de sécurité de l'information dans les systèmes temps réel.

8 décembre 2005
Ismaïl Berrada (LaBRI)
Modélisation, Analyse et Test des Systèmes Communicants à Contraintes Temporelles: Vers une Approche Ouverte du Test
Cette thèse porte essentiellement sur l'application des méthodes formelles pour la génération de test.

En premier lieu, nous introduisons le modèle CS comme une description des systèmes communicants. Le modèle CS est basé sur la séparation entre de la description des entités d'un système communicant (le flux propre des entités est exprimé à l'aide des automates temporisés étendus) et la description des communications et du partage des ressources entre ces dernières (le flux partagé est exprimé à travers une topologie de communication).

En deuxième lieu, nous abordons l'analyse des systèmes temporisés, en particulier, l'extraction des diagnostics temporisés pour un chemin symbolique. D'une part, nous montrons comment extraire des valuations à partir d'une matrice de bornes (DBM). Notre solution est basée sur l'identification des valuations des bornes. Ces dernières permettent de couvrir les bornes d'une DBM canonique avec un nombre linéaire de valuations. D'autre part, nous proposons un deux approches pour générer des diagnostics temporisés d'un chemin symbolique. La première solution considère le polyèdre de contraintes associé à un chemin. Quant à la deuxième approche, elle utilise une analyse symbolique en avant et en arrière.

En troisième lieu, nous considérons la génération automatique des tests temporisés. Nous introduisons un cadre formel, comportant une définition de la notion de conformité pour les systèmes temporisés et une approche de génération automatique des tests de conformité.

En quatrième lieu, nous proposons une modélisation uniforme des différents types, approches et architecture de test. Cette modélisation est basée sur les algorithmes générique de génération et la définition d'un critère de couverture structurelle sous forme de coloriage (ordonné) de graphe. Comme conclusion de cette partie, nous introduisons la notion de test ouvert.

Finalement, nous présenterons l'outil TGSE (Test Generation, Simulation and Emulation) développé dans le cadre du projet Calife et l'étude de cas CSMA/CD.

1 décembre 2005
Gregor Goessler (INRIA Rhône-Alpes)
Component-based construction of reactive systems in Prometheus
Component-based modeling is crucial to overcome the complexity of embedded systems. However, two major obstacles need to be addressed: the heterogeneous nature of the models, and the lack of results to guarantee correction of the composed system. The heterogeneous nature comes from the fact that it is usually necessary to compose different parts of the system on different levels of abstraction, and using different models of interaction (e.g., blocking or non-blocking, rendez-vous or broadcast) and models of execution (e.g., asynchronous or run-to-completion). In this talk we present a general model for component-based construction of heterogenous reactive systems. Each component consists of three layers: (1) a description of its behavior, (2) an interaction model describing the topology of the system and the types of interactions between the components, and (3) an execution model specifying constraints relative to scheduling and resource management. A commutative and associative composition operation allows for incremental modeling of the system. The second part of the talk is dedicated to the Prometheus tool, which implements the framework along with a set of verification and synthesis algorithms.
17 novembre 2005
Emmanuel Fleury (LaBRI)
TiGa: Timed Games for Everyone!
Uppaal TiGa (TImed GAme) is part of the Uppaal tool family (Uppaal, Uppaal Cora and Uppaal TiGa). Uppaal TiGa is designed for synthesizing winning strategy for timed games. The games are specified as a network of Timed Game Automata (TGA) through an augmented Uppaal user-interface. The verification part of the GUI has been modified to define winning or losing conditions allowing the user to solve reachability and safety timed games.

The analysis of the timed game and the synthesis of the winning strategy is performed by a totally new engine based on the on-the-fly algorithm presented in [1] and using the Uppaal DBM library. Since the publication of [1], huge improvements have been accomplished bringing up the hope that more realistic models can be analyzed. The input language allow the user to use templates, boolean and integer variables. Of course, in the long term, Uppaal TiGa is expected to support all the features of the Uppaal language.

[1] F. Cassez, A. David, E. Fleury, K. G. Larsen, and D. Lime. Efficient on-the-fly algorithms for the analysis of timed games. In Proc. 16th Int. Conf. Concurrency Theory (CONCUR'05), San Francisco, CA, USA, Aug. 2005, volume 3653 of Lecture Notes in Computer Science, pages 66-80. Springer, 2005.

10 novembre 2005
Antoine Rollet (LaBRI)
Du test de conformité au test de robustesse
Le test de robustesse est un domaine récent en comparaison aux autres formes de test connues, comme par exemple le test de conformité. Dans ces deux domaines, la prise en compte du temps est toujours un enjeu de recherche. Après avoir rappelé les grands principes du test de conformité, une méthode de génération sera présentée. Cette méthode cherche à identifier un état de la spécification dans l'implantation. Ensuite, la problématique du test de robustesse sera abordée, et une approche sera exposée. Cette dernière se base sur l'idée que l'on a deux spécifications du système, une nominale et une dégradée, et on cherche à s'assurer que le comportement du système en situation "hostile" respecte bien au moins celui de la spécification dégradée.
3 novembre 2005
Marc Zeitoun (LaBRI)
Controller synthesis problem for distributed systems
A controller is a piece of software observing the behavior of an open system, in order to guide the system so that it meets some given specification. The controller synthesis problem consists in designing an algorithm to build a controller from a system and a specification.

This talk first surveys some results in this area for distributed systems, under synchronous or asynchronous semantics. While the problem is decidable for finite state sequential systems and regular specifications, it is usually undecidable for finite state distributed ones.

We show how to weaken requirements on the controller so that the problem becomes decidable for some classes of systems and specifications. More precisely, we give an interpretation of the controller synthesis problem in terms of team games, and we show that such distributed games are decidable with an appropriate notion of memory.

Joint work with Paul Gastin, Benjamin Lerman and Nathalie Sznajder.

20 octobre 2005
Bernard Boigelot (Univ. Liège)
Generic Acceleration by Iterating Automata
We consider the problem of computing exactly the set of reachable configurations of an infinite-state system. A natural solution consists in exploring symbolically the reachability graph of the model under study, using acceleration techniques for computing in finite time infinite sets of reachable configurations. There are several ways of performing such an acceleration. A first possibility is to study the iteration of the data transformations labeling the control cycles. This method gives good results, but is very specific to the data domain of the system, as well as to the data operations that are carried out. In this talk, we will present another approach to accelerating symbolic state-space exploration, based on computing the limit of sequences of automata. This method has the advantage of being applicable to a broader class of models than those handled by specific techniques. The talk will describe a generic acceleration algorithm, and discuss some implementation issues.

Joint work with Axel Legay and Pierre Wolper.

13 octobre 2005
Jérôme Leroux (LaBRI)
The convex hull of a Number Decision Diagram is a computable polyhedron
A Number Decision Diagram (NDD) is an automaton that represents regular set of integer vectors encoded as strings of digit vectors (least or most) significant digit first.

In this presentation, we provide an algorithm for computing the convex hull of the set represented by a NDD. As any Presburger-definable set (a set defined in the first additive theory of the integers) can be efficiently represented by such an automaton, we deduce an algorithm for automatically computing the convex hull of any set of vectors defined by such a formula.

The convex hull is central in many applications: in the area of abstract interpretation, controller synthesis, test-generation and verification.

Example: Let X be the set defined by the following Presburger formula F: F(x,y):=\exists z. (x>y AND x+y=2.z) The convex hull is defined by x >= y+2 and not by x >= y+1. After the presentation, you should be able to compute this constraint automatically.

29 septembre 2005
Igor Walukiewicz
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: Mon Jan 2 17:02:40 CET 2006