30 mai 2002 |
Alain Griffault
|
23 mai 2002 |
Luigi Santocanale
Un jeu de parité est joué sur un graphe fini de positions et de
mouvements. Dans ce graphe on peut bien avoir des cycles, et pourtant on
définit l'ensemble des chemins inifinis gagnants pour un des deux
joueurs à l'aide de la ``condition de parité''. Cette condition est bien
connue dans la théorie des automates qui reconnaissent les objects
infinis. En effet tout automate est équivalent à un automate qui utilise
la condition de parité. Nous allons définir cette condition et lui
donner une interprétation algébrique à l'aide des notions d'algèbre
initiale et coalgèbre finale d'un foncteur, c-à-d., à l'aide des
formulations catégorielles de l'induction et de la coinduction. Nous
allons associer une expression algébrique à chaque jeu de parité et
montrer qu'elle dénote (dans la catégorie des ensembles) l'ensemble des
stratégies gagnantes pour un des deux joueurs. Nous montrons aussi que
les expressions associés aux jeux sont équivalentes aux expressions
qu'on peut engendrer par les operations de produit fini, de coproduit
fini, d'algèbre initiale et coalgèbre finale, c.à-d aux µ-termes
catégoriels. Nous obtenons cette façon une caractérisation explicite de
tous les foncteurs qu'on peut définir par des µ-termes dans la catégorie
des ensembles.
|
16 mai 2002 |
Sardaouna Hamadou
Nous présentons dans ce travail, un protocole de transaction électronique
sécuritaire et surtout anonyme par l'association d'un logiciel de cryptage
et d'une carte à puce. La sécurité est assurée par l'utilisation des
techniques cyptographiques telles que le chiffrage, la signature électronique
et l'authentification. L'anonymat est assuré par le fait que le client ne
révèle au marchand aucune information pouvant l'identifier tout en
garantissant la quasi-impossibilité d'une fraude.
|
18 avril 2002 |
Jean-Claude Royer
Une préoccupation actuelle en spécification concerne les systèmes mixtes
ou hétérogènes, i.e. des systèmes avec à la fois des aspects dynamiques
et des types de données.
Ce problème apparaît en spécification formelle mais aussi dans le
contexte des méthodes de développement comme UML par exemple.
Dans ce domaine nous avons proposé le couplage d'un système de
transition symbolique et d'une spécification algébrique que nous avons
appelé Type Abstrait Graphique.
Nous montrons les principes de la spécification sur un exemple simple de
distributeur de boisson et nous commenterons quelques propriétés de la
spécification produite.
Nous aborderons ensuite une approche basée sur la logique du premier
ordre et permettant d'écrire des propriétés de logique temporelle et
d'en faire la preuve en utilisant par exemple Larch Prover ou PVS.
En dernier lieu nous esquisserons quelques liens connus avec la logique
temporelle CTL* et quelques résultats concernant l'automatisation des
preuves.
|
11 avril 2002 |
Michaël Adélaïde
Les systèmes hybrides permettent de modéliser des processus dont le
comportement est une succession d'évolutions continues et de transitions
discrètes. Les applications mises en oeuvre en Informatique Temps-Réel
en font partie. Etant donnée une spécification des contraintes P à
réaliser, le designer représente les applications sous la forme
d'automates hybrides.
Avant la mise en service de ces programmes, il est nécessaire de
vérifier que les contraintes sont été respectées.
Les outils de la vérification "traditionnelle" renvoient des réponses
booléennes : les contraintes sont ou ne sont pas respectées.
Pour l'analyse paramétrique, les constantes du système (vitesses,
délais,...) ne sont pas fixées dès le départ. Le problème à résoudre est
de trouver les valeurs de ses constantes pour lesquelles la propriété P
est vérifiée.
La première approche consiste à paramétrer l'outil permettant de vérifier les systèmes sans paramètres. On peut définir un processus mécanique pour cette transformation. Il consiste à utiliser des types qui correspondent à la "non-évaluation" des formules sur le type original. Si on veut paramétrer des entiers sur lesquels on n'effectue que l'addition et la multiplication, on utilise l'anneau des polynômes à coefficients entiers (les inconnues étant les paramètres). Cependant, les restrictions suivantes apparaissent :
|
4 avril 2002 |
Bernard Boigelot
This talk introduces finite-automata based algorithms for handling
linear arithmetic with both real and integer variables. Previous work
has shown that this theory can be dealt with by using finite automata
on infinite words, but this involves some difficult and delicate to
implement algorithms. The contribution of this work is to show, using
topological arguments, that only a restricted class of automata on
infinite words are necessary for handling real and integer linear
arithmetic. This allows the use of substantially simpler algorithms.
These algorithms have been implemented in a verification tool for
programs relying both integer and real variables.
Joint work with S. Jodogne and P. Wolper. |
21 mars 2002 |
Giacomo Lenzi
We consider modal mu calculus, a logic introduced by Kozen in 1983.
Modal mu calculus is the extension of modal logic with two operators which
give the least and greatest fixpoints of monotone functions from sets to sets.
Modal mu calculus is considerably expressive, and it is widely used in system
verification.
Recall that a logic is said to ``have interpolation'' if for every two
formulas A, C with A => C (where => denotes logical implication),
there is an ``interpolant'' formula B in the common language of A and C such
that A => B => C. For instance, first order logic has interpolation.
However, mu calculus not only has interpolation, but it has also a stronger property called ``uniform interpolation'': that is, for every formula A and for every language L, there is a ``uniform interpolant'' formula I(A,L), in the language L, such that:
In this talk we will present this theorem, we will sketch the proof, and we will give some motivations, applications and related work. |
14 mars 2002 |
Ahmed Bouajjani
We present a tool for automatic analysis of infinite-state systems
modeled by means of extended automata.
The models that can be analysed are parametric clocks and counters automata
communicating through lossy FIFO-channels.
The tool, called TREX, uses symbolic representations for infinite-state
domains
(regular expressions, parametric DBMs, arithmetical constraints),
and forward/backward reachability analysis procedures,
enhanced with acceleration techniques in order to help termination.
TREX allows on-the-fly verification of safety properties,
the generation ofthe reachability set which can be used, e.g.,
for parameter synthesis and for invariant generation,
and the construction of a finite symbolic graph which can be used for
finite-model checking.
The tool is interfaced with the IF environment allowing
to use SDL as a specification language, and to interact
with abstraction tools and finite model-checkers.
Travail commun avec Aurore Annichini-Collomb et Mihaela Sighireanu. |
21 février 2002 |
Jean-Michel Couvreur
|
14 février 2002 |
Jean-Michel Couvreur
|
7 février 2002 |
Alain Finkel
Calculer effectivement une représentation symbolique de
l'ensemble des états accessibles d'un système paramétré ou infini est
une question centrale en vérification. Nous étudierons des modèles
indécidables en général mais pour lesquels les accélérations sont quand
même calculables. Nous montrerons que l'utilisation du cadre des
accélérations et des représentations symboliques permet de verifier un
certain nombre de protocoles bien connus. L'outil FAST, en cours de
développement, a permis de réaliser des expériences très encourageantes
sur la plupart des protocoles de diffusion (broadcast protocols).
|
31 janvier 2002 |
Vlad Rusu
Applying formal methods to testing has recently become a popular
research topic. In this talk we demonstrate the opposite approach,
namely, applying testing techniques to formal verification. The
idea is to use symbolic test generation techniques to extract
subgraphs (called "components") from a specification and to perform
the verification on the components rather than on the whole system.
This may considerably reduce the verification effort and, under
reasonable sufficient conditions, a safety property verified on a
component also holds on the whole specification. We demonstrate the
approach by verifying an electronic purse system using our symbolic
test generation tool STG and the PVS theorem prover.
URL: http://www.irisa.fr/pampa/perso/rusu/draft/ |
24 janvier 2002 |
André Arnold
|
17 janvier 2002 |
Franck Cassez
In the literature, we find several formulations of the control problem for
timed and hybrid systems.
We argue that formulations where a controller can cause an action at any
point in dense (rational or real) time are problematic, by presenting an
example where the controller must act faster and faster, yet causes no Zeno
effects (say, the control actions are at times
0, 1/2, 1, 1 . 3/4, 2, 2 . 7/8, 3, 3 . 15/16, ...).
Such a controller is, of course, not implementable in software.
Such controllers are avoided by formulations where the controller can cause
actions only at discrete (integer) points in time.
While the resulting control problem is well-understood if the time unit, or
``sampling rate'' of the controller, is fixed a priori, we define a novel,
stronger formulation:
the discrete-time control problem with unknown sampling rate
asks if a sampling controller exists for some sampling rate.
We prove that, surprisingly and unfortunately, this problem is undecidable
even in the special case of timed automata.
Joint work with Tom Henzinger (EECS Department, University of California at Berkeley, USA) and Jean-François Raskin (Département d'Informatique, Université Libre de Bruxelles, Belgium). To appear in HSCC'02. |
10 janvier 2002 |
Claude Jard
La synthèse de cas de test pour le test de conformité de composants
communicants a été principalement tournée vers la production de cas
de test séquentiels. Dans le contexte des systèmes répartis, il est
utile d'étendre ces techniques pour générer des testeurs multiples.
Nous fondons ce travail sur notre expérience dans l'utilisation de
techniques de model-checking, implantées avec succès dans l'outil
TGV (Irisa/Vérimag) de génération de tests. Dans le prolongement des
travaux de A. Ulrich et H. König, nous proposons d'utiliser un
modèle de vrai-parallélisme basé sur le dépliage de graphes. La
conférence présente les principes d'une chaîne complète de synthèse,
depuis la définition d'objectifs de test jusqu'à la production d'un
test projeté sur un ensemble de testeurs.
|
20 décembre 2001 |
Eugene Asarin
Many properties of hybrid systems are algorithmically undecidable. In
practice however, systems are only known up to a certain degree of accuracy
and are subject to noise and perturbations. I will consider various
classes of hybrid systems and will analyse how noise affects decidability
for these classes. This presentation will be based on recent attempts by
Asarin-Bouajjani, Henzinger-Raskin and others to formalize the impact of
noise on computational capabilities of hybrid systems.
|
6 décembre 2001 |
Frédéric Herbreteau
Les systèmes réactifs évoluent suivant les sollicitations (événements discrets)
de leur environnement. La programmation asynchrone de telles applications
nécessite de mémoriser les événements qui ne peuvent pas être traités lorsqu'ils
surviennent. Les automates à file réactifs (AFR) permettent de modéliser de
telles applications.
Qu'il s'agisse d'implantation ou de vérification, il est alors important de s'assurer de la bornitude de ces automates. Bien entendu, cette propriété dépend du rythme des occurrences des événements. Cette dernière spécification fait défaut aux AFR, c'est pourquoi, nous considérons les automates à file réactifs embarqués, qui comblent cette lacune. Nous étudions divers problèmes de vérification pour les AFR embarqués, et en particulier, nous montrons que le problème de la bornitude est généralement indécidable. Ceci nous conduit à définir un test pour ce problème. Nous considérons ensuite la spécification de l'environnement sous la forme d'un système hybride, et nous adaptons notre test dans ce contexte. |
29 novembre 2001 |
Bertrand Tavernier (CRIL Technology)
|
22 novembre 2001 |
Kaninda Musumbu
Alose (Automatisation de Logigrammes de Securité) est un simulateur de systèmes
de sécurité écrit en Java exploité par une interface graphique écrite en
Java Swing. Son usage est destiné à la vérification de systèmes de sécurité
déjà existants ou en cours de conception. Ces fonctionnalités font de ce
simulateur un outil qui permet de vérifier la cohérence d'un système de sécurité.
L'exposé a pour objet de présenter la base théorique d'ALose.
|
15 novembre 2001 |
Patrick Félix
Calife (Environnement pour la Preuve formelle et le Test
d'Algorithmes utilisés en Télécommunication) est un projet de recherche
RNRT dont l'objectif est de développer un prototype offrant un environnement
pour la spécification, la vérification formelle et la génération de tests de
systèmes avec des contraintes temporelles. Un modèle de spécification, appelé
p-automates (une variante des systèmes hybrides linéaires) a été développé dans
le cadre du projet Calife pour exprimer un système. Une des contributions de
l'équipe concerne l'intégration d'outils de générations de séquences de tests
dans cette plate-forme commune.
Les approches de génération automatique de séquences de test temporisées peuvent de décomposer selon les trois catégories suivantes :
Cet exposé traitera des points 1 et 2. Le point 3 sera abordé lors d'un autre exposé (Davy Rouillard) dans le cadre de ce groupe de travail. |
8 novembre 2001 |
Alain Griffault
|
25 octobre 2001 |
Aymeric Vincent
Cette présentation se base sur un article publié à MSR 2001 et
montrera le lien qui unit le problème de la synthèse de contrôleurs et
le calcul d'une stratégie gagnante dans un jeu de parité.
|
18 octobre 2001 |
André Arnold
I. La théorie de Ramadge et Wonham.
|
11 octobre 2001 |
Grégoire Sutre
One approach to model checking software is based on the
abstract-check-refine paradigm:
build an abstract model, then check the desired property, and if the
check fails, refine the model and start over.
We introduce the concept of lazy abstraction to integrate and
optimize the three phases of the abstract-check-refine loop.
Lazy abstraction continuously builds and refines a single abstract model
on demand, driven by the model checker, so that different parts of the
model may exhibit different degrees of precision, namely just enough to
verify the desired property.
We present an algorithm for model checking safety properties using lazy
abstraction and describe an implementation of the algorithm applied to
C programs.
|
4 octobre 2001 |
André Arnold
|