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




Séance du jeudi 15 décembre 2005


Relâche




Prévisions





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


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: Sat Dec 10 11:53:39 CET 2005