24 juin 2004 |
Frédéric Herbreteau
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
|
10 juin 2004 |
Manuel Baclet
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
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
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
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
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
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é est un mu-calcul qui contient à la
fois les modalités
"évènementielles" habituelles et [a] et les modalités temporelles
"Until" et "Always" de la logique LTL (sur les réels). Il est aux
automates temporisés ce que la mu-calcul modal classique est aux
automates discrets.
On montrera comment la régionalisation permet, par transfert de compétences, de rendre ce mu-calcul équivalent au mu-calcul modal classique. |
18 mars 2004 |
Michaël Adélaïde
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 :
|
11 mars 2004 |
André Arnold
|
4 mars 2004 |
Xavier Briand
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
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
|
15 janvier 2004 |
Thierry Jéron
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:
|
8 janvier 2004 |
César Viho
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
|
20 novembre 2003 |
Claire Pagetti
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
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
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
.
|
9 octobre 2003 |
Grégoire Sutre
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. |