2003 - 2004

Groupe de travail

Modélisation, Vérification et Tests des systèmes informatisés
&
Petite école pour la vérification

Le jeudi de 11h à 12h15
Salle G.T. 2, LaBRI, Rez-de-chaussée




Programme du jeudi 1 juillet 2004


Relâche





Prévisions





Réunions précédentes (2003 - 2004)

24 juin 2004

Frédéric Herbreteau
AltaRica Hybride .

AltaRica est un formalisme de modélisation de systèmes réactifs orienté composants (par exemple, une pile éléctrique ou une ampoule). Ceux-ci peuvent ensuite être composés hiérarchiquement pour former de nouveaux composants. Ils communiquent entre eux via la synchronisation, et via l'échange de flux (par exemple, le courant éléctrique passant d'une pile éléctrique à une ampoule). Dans la version actuelle d'AltaRica, le mode d'évolution des flux est abstrait (par exemple, courant présent ou absent). Nous nous attachons, dans la version hybride d'AltaRica, à permettre la spécification des lois d'évolution des flux (par exemple, la décharge de la pile au cours du temps et le courant résultant en fonction du temps). Nous présenterons l'état d'avancement de nos travaux.
17 juin 2004

Stéphanie Gaudan, The Quang Tran, Joseph Tylutki
Pré-soutenances de mémoire de recherche .

  • Stéphanie Gaudan
    Abstraction par prédicats de systèmes de transitions symboliques

  • The Quang Tran
    Finite Unfoldings of Well-Structured Data Nets

  • Joseph Tylutki
    Manipulation des contraintes dans le formalisme AltaRica
10 juin 2004

Manuel Baclet
Modélisation et vérification des systèmes sur puce, exemple d'un composant d'IDCT .

La complexité croissante des systèmes sur puces (SoCS), due à l'augmentation (exponentielle) du nombre de transistors pouvant être intégrés sur une puce, a entraîné le développement de méthodes permettant de valider la conception avant la fabrication. Actuellement, la méthode la plus utilisée est fondée sur la simulation logicielle des systèmes. Il est donc important de disposer de techniques faciles à mettre en oeuvre et assurant des simulations précises et efficaces. A cette fin, nous proposons un formalisme à base d'automates finis (les i/o-automates) qui permet de modéliser les séquences d'entrées/sorties d'un composant sur puce. Pour lutter contre l'explosion combinatoire, nous réalisons l'abstraction suivante: nous oublions les valeurs des données et nous considérons seulement des événements du type "une donnée entre dans le composant et une donnée sort" ou "une donnée entre mais aucune ne sort", etc. Ce formalisme peut être utilisé pour décider si deux composants, supposés implanter la même fonction, ont les mêmes comportements d'entrées/sorties, de sorte que l'un peut être remplacé par l'autre, ou encore pour obtenir automatiquement, à partir d'une description de haut niveau du composant, un programme qui simule son fonctionnement précisément (au niveau des "transferts de registres"). Nous illustrons l'utilisation des i/o-automates sur l'exemple d'IDCT, un composant de traitement du signal.
27 mai 2004

Dominique Cansell
Formal Construction of a Non-blocking Concurrent Queue Algorithm .

After a short presentation of the concept of "event system" (as encoded within B), we present a development of a non-blocking and concurrent algorithm by M.M Michael and M.L. Scott. Many processes share a non-empty queue and can dequeue the first value and/or enqueue a new value at the queue. Every processes progress on atomic actions so its extremely difficult to assume the correction of this algorithm. Using refinement we discover problems and solve them like the well known ABA problem. We have also found some errors in one guard of the algorithm and also remove some of them.

Joint work with Jean-Raymond Abrial.

13 mai 2004

Jean-Michel Couvreur
Une structure de données partagée pour manipuler les automates .

Applying the BDD principle to automaton is not that easy. Indeed, the notion of minimal automaton does not lead to constant-time comparison. Moreover, all existing BDD-extensions have an acyclic directed graph structure, while an automaton may have cycles. In this paper we propose a new data structure, called shared automata, for representing deterministic finite automata (DFA). Shared automata admit a strong canonical form for DFA similarly to Binary Decision Diagrams (BDDs). As a result, checking whether two DFAs are equal is a constant-time comparison. A hash-based cache may be used to improve significantly the performance of automata operations. The key points of this structure are the decomposition of the DFA into its strongly connected components and an incremental algorithm based on this decomposition for transforming any DFA into a shared automaton. We experimentally compare PresTaf, a direct implementation of the Presburger arithmetic built on a shared automata package, and the Presburger package LASH based on standard automata algorithms. Experimental results show the great benefit of the new canonical data structure applied to symbolic state space exploration of infinite systems.
6 mai 2004

Franck Cassez
Stratégie optimale pour les jeux temporisés avec coût .

Priced timed (game) automata extends timed (game) automata with costs on both locations and transitions. In this paper we focus on reachability games for priced timed game automata and prove that the optimal cost for winning such a game is computable under conditions concerning the non-zenoness of cost. Under stronger conditions (strictness of constraints) we prove in addition that it is decidable whether there is an optimal strategy in which case an optimal strategy can be computed. Our results extend previous decidability result which requires the underlying game automata to be acyclic. Finally, our results are encoded in a first prototype in HyTech which is applied on a small case-study.

[BCFL04] P. Bouyer, F. Cassez, E. Fleury and K. G. Larsen. Optimal Strategies in Priced Timed Game Automata. BRICS Research Report RS-04-4. 2004.

8 avril 2004

Claire Pagetti
Extension temps réel d'AltaRica .

Le travail présenté s'inscrit dans la continuité de l'étude du langage de description de systèmes AltaRica. Ce langage, développé au Labri, permet de modéliser des systèmes réels de manière hiérarchique. L'objectif est d'introduire le temps quantitatif dans le but de concevoir des systèmes temps réel, c'est à dire des systèmes assujettis à des contraintes temporelles et de proposer des moyens de vérifier les modèles obtenus.

Nous exposerons deux extensions du langage: une version temporisée et une hybride. Ces extensions respectent les caractéristiques du langage initial et conservent les aspects de hiérarchie, de synchronisation, de partage de variables et de priorité statique. En outre, afin d'améliorer les descriptions temps réel, de nouveaux opérateurs de modélisation, comme l'urgence et les priorités temporelles, ont été ajoutés. Nous obtenons ainsi un langage hiérarchique de haut niveau de modélisation de systèmes temps réel.

Nous détaillerons particulièrement la sémantique du langage, le pouvoir d'expression des langages AltaRica temps réel et les moyens de traductions automatiques vers des modèles classiques existants. Ces algorithmes reposent sur la notion de mise à plat de modèle, i.e. réécrire un modèle sans sous composant.

Enfin, nous montrerons comment vérifier des propriétés sur des modèles AltaRica temporisé à l'aide d'un prototype qui étant donné un modèle le met à plat puis le traduit en automate temporisé au format du model checker UPPAAL.

1 avril 2004

Guillaume Gardey
IRCCyN (EC Nantes) .

Les réseaux de Petri T-Temporels consituent une extension temporelle des réseaux de Petri. La méthode classique d'analyse de tels réseaux est basée sur la technique du graphe des Classes (B.Berthomieu et M.Diaz) mais elle est inadaptée pour la vérification de certaines propriétés qualitatives (branchement) et quantitatives. Cet exposé décrit une méthode permettant de calculer plus efficacement l'espace d'état d'un réseau de Petri T-Temporel borné ainsi que sa traduction en automate temporisé. Cette approche permet ainsi d'envisager la vérification de propriétés quantitatives.
25 mars 2004

André Arnold
Le mu-calcul modal temporis .

18 mars 2004

Michaël Adélaïde
Modélisation de réseaux de régulation génétique .

Toutes les informations nécessaires au fonctionnement d'une cellule sont contenues dans son ADN. Une des activités principales de la cellule est la fabrication de protéines. Cependant, cet ADN n'est pas directement utilisé pour la synthèse de protéines. Il est d'abord transcrit en ARN, ARN traduit en protéines.

Le flux génétique est ce transfert d'information de l'ADN vers les protéines. La régulation régulation génétique est le contrôle par la cellule de l'opération de transcription (i.e. le pasaage ADN->ARN).

On s'intéresse à la modélisation dynamique de la régulation génétique. Plusieurs modèles ont été proposés. Ils représentent différents niveaux d' "abstraction" du comportement cellulaire. L'exposé est essentiellement bibliographique. A partir d'une représentation des interactions moléculaires intervenant dans la cellule procaryote (bactérie), on présentera principalement les modèles de Savageau, Brazma et Schlitt, De Joong et Thomas. L'objectif est de présenter les deux principaux problèmes informatiques à résoudre, à savoir :

  • synthèse de modèles à partir de relevés d'expériences (reverse engineering)
  • comparaison de modèles (abstraction, ...)
  • modélisation hybride
11 mars 2004

André Arnold
Une proposition de définition générale des systèmes hybrides .

4 mars 2004

Xavier Briand
Contrôle avec événements indiscernables et inobservables .

La théorie du contrôle a pour objet d'étudier la possibilité et les moyens de transformer des systèmes afin qu'ils puissent vérifier des spécifications. Les différents types de problèmes de la théorie du contrôle seront présentés pour situer le "contrôle dynamique avec évènements inobservables et indiscernables".

Afin de présenter la décidabilité du problème de contrôle centralisé, un formalisme plus expressif que le mu-calcul est utilisé (qui prend en compte les notions d'inobservabilité et d'indiscernabilité). Enfin, l'indécidabilité du problème de contrôle décentralisé ainsi que des cas décidables seront présentés.

19 février 2004

François Bréant
Diagrammes de décision de données (DDD): application à la vérification du modèle ferroviaire BART .

La bibliothèque des DDDs implémente une structure de données pour représenter des ensembles finis de séquences d'affectations ainsi que les opérations de construction associées. La représentation compacte des données et l'utilisation de caches permet de calculer des ensembles d'états très grands.

Dans cette étude de cas, le système ferroviaire BART a été modélisé dans un langage de haut niveau comprenant les appels de procédure distant et la communication par envoi de messages. Une application de calcul des états accessibles de ce modèle a été implémentée au moyen de la bibliothèque des DDDs.

L'objectif de notre étude était de démontrer la capacité des DDDs à représenter l'ensemble des états accessibles d'un système de taille moyenne comportant de nombreuses composantes dynamiques telles que les files de messages, les piles d'exécution, l'instanciation dynamique d'objets. Quelques problèmes et les solutions trouvées seront détaillés.

29 janvier 2004

Sébastien Grivet
Algorithmes pour la construction de dépliages de réseaux de Petri saufs. .

15 janvier 2004

Thierry Jéron
Génération de test, vérification et contrôle de systèmes réactifs .

Dans une première partie, nous rappelons brièvement la problématique du test de conformité, les modèles, la théorie du test et les principes de la génération de tests sur lesquels se fondent l'outil TGV. La génération de tests consiste principalement à sélectionner des comportements d'une spécification comportementale à partir d'objectifs de test decrivant des propriétés d'accessibilité. Nous mettrons l'accent sur la similitude avec la synthèse de contrôleurs pour ce type de propriété.

Dans le même cadre théorique, on s'est récemment intéressés à des objectifs de test exprimant des propriétés de sûreté. Dans ce cadre nous montrons une relation forte entre la conformité d'une implémentation à une spécification, et la satisfaction de ces propriétés par la spécification et par l'implémentation. Plus précisément, pour la relation de conformité ioco, une implémentation I est conforme à sa spécification S si pour toute propriété satisfaite par S, la propriété "restreinte" à S est aussi satisfaite par I. On en déduit une technique de génération de tests pour ces objectifs de sûreté produisant des tests détectant à la fois la non conformité et la violation de propriétés de sûreté. Ces résultats permettent d'envisager un continuum entre vérification de propriétés sur la spécification, génération de tests à partir de la spécification et des propriétés, et test des propriétés de sûreté.

Toujours dans le même cadre théorique, on s'intéresse ensuite à un problème de contrôle de conformité. Etant donné une spécification S et une implémentation I non-conforme à S pour ioco, mais que l'on peut partiellement contrôler (boîte blanche), le problème consiste à contrôler I pour assurer sa conformité à S.

On terminera par quelques reflexions sur la relation entre synthèse de contrôleurs et test de conformité.

Bibliographie:

  • V. Rusu, H. Marchand, V.Tschaen, T. Jéron, B. Jeannet From safety verification to safety testing, in Testcom'04, Oxford, March 2004
  • T. Jéron, H. Marchand, V. Rusu, V. Tschaen, Ensuring the conformance of reactive discrete-event systems using supervisory control, in 42nd IEEE Conference on Decision and Control, Hawaii, USA, Décembre 2003.
8 janvier 2004

César Viho
First steps towards formal interoperability testing .

A lot of work has been done in conformance testing which led to precise formal characterizations of conformance - specially through the notion of conformance relations - and a framework for conformance testing. Unfortunately, this is still not yet the case for interoperability testing.

I will present our recent work which tries to prove that the existing concepts of conformance testing can be used to define a formal framework for interoperability testing. First, the different possible interoperability testing architectures will be discussed. Then, I will present formal definitions of the notion of interoperability that we proposed, by the way of the so-called "interoperability relations" based on the existing conformance relation ioconf defined (by Jan Tretmans) for conformance testing. An interoperability relation specifies formally the conditions to be satisfied by two or more implementations to be able to interoperate. A comparison of these interoperability relations will be given, in terms of their power to detect non interoperability. Using one of the important results of this comparison, this presentation will end with some guidelines to help in generating efficiently interoperability tests.

27 novembre 2003

Aymeric Vincent
Conception et réalisation d'un vérificateur de modèles AltaRica .

20 novembre 2003

Claire Pagetti
Le temps réel dans AltaRica .

La première étape du processus de vérification des systèmes est la modélisation du système. Les outils existants pour les systèmes temps réel prennent en entrée des réseaux d'automates temporisés ou hybrides, donc sans hiérarchie. Dans cet exposé, nous montrons comment introduire la notion de temps dans les modèles AltaRica et nous construisons ainsi un langage hiérarchique de modélisation de systèmes réactifs temps réel, Timed AltaRica. Les différentes étapes seront illustrées à l'aide d'un exemple de commande d'une gouverne. Les modèles obtenus ont la même expressivité que les automates temporisés avec mise à jour. Nous montrerons comment traduire un modèle TAR en un automate temporisé. Cette traduction est implantée dans un outil ce qui permet de vérifier des propriétés sur les systèmes modélisés à l'aide du model checker Uppaal. Enfin, la notion de priorité AR est étendue de façon à prendre en compte le temps. Nous ajoutons l'urgence et les priorités temporelles dans les modèles.
13 novembre 2003

Serge Autexier
Formal Software Development in MAYA .

The formal development of industrial-size software is an error-prone and therefore an evolutionary process. Verifying formal specifications usually reveals hidden errors causing the change of parts of the specification. Also adding new functionality will result in changes of the specification which always endangers the verification work already done. In this talk we describe the system MAYA which maintains formal developments. The MAYA-system supports an evolutionary formal development since it allows users to specify and verify developments in a structured manner, incorporates a uniform mechanism for verification in-the-large to exploit the structure of the specification, and maintains the verification work already done when changing the specification. MAYA relies on development graphs as a uniform representation of structured specifications, which enables the use of various (structured) specification languages to formalize the software development. Moreover, MAYA allows the integration of different theorem provers to deal with the actual proof obligations arising from the specification, i.e. to perform verification in-the-small.
23 octobre 2003

Michaël Adélaïde
Analyse paramétrique des systèmes hybrides .

L'analyse paramétrique des systèmes hybrides consiste à trouver les contraintes sur les paramètres qui assurent un bon fonctionnement de ces systèmes. Les paramètres représentent des constantes réelles. Pour un problème paramétrique donné, un semi-algorithme est obtenu en transformant un outil résolvant le problème non paramétrique correspondant. On recherche alors des conditions sur les systèmes hybrides paramétriques, conditions qui assurent la terminaison de l'outil paramétrique. A cet effet, nous avons introduit les systèmes hybrides faiblement contrôlés. Il s'agit de systèmes paramétriques dont chaque cycle possèdent une arête qui réinitialise toutes les variables qui ne sont pas des paramètres. Le problème de l'accessibilité est alors décidable pour les systèmes hybrides rectangulaires faiblement contrôlés ainsi que tout problème du « mu-calcul » pour les systèmes hybrides faiblement contrôlés à évolutions continues polynomiales (les évolutions des variables sont des polynomes du temps écoulé dans le noeud courant).
16 octobre 2003

Réunion de rentrée .

  • Présentation des nouveaux membres.
  • Bilan de l'activité de l'équipe.
  • Préparation du programme du GT.
9 octobre 2003

Grégoire Sutre
An optimal automata approach to LTL model checking of probabilistic systems .

Most verification problems on finite systems may be formulated and solved optimally using automata based techniques. Nonetheless LTL verification of (finite) probabilistic systems, i.e. deciding whether a probabilistic system almost surely satisfies an LTL formula, remains one of the few exceptions to this rule. As a matter of fact, existing automata-based solutions to this problem lead to double EXPTIME algorithms, while Courcoubetis and Yannakakis provide an optimal (non automata-based) one in single EXPTIME. In this study, we remedy this exception.

Our optimal automata based method proceeds in two steps: we present a minimal translation from LTL to omega-automata and point out appropriate properties on these automata ; we then show that checking whether a probabilistic system satisfies an omega-automaton with positive probability can be solved in linear time for this kind of automata. Moreover we extend our study to the evaluation of this probability. Finally, we discuss some experimentations with our implementation of these techniques: the ProbaTaf tool.

Joint work with Jean-Michel Couvreur and Nasser Saheb.




Archives des années précédentes





Navigation




Last modified: Wed Jun 30 16:20:45 CEST 2004