Proposition de Travaux d'Etude et de Recherche
Maîtrise 1999-2001
Sujet :
Etude comparative sur les structures de données utilisées pour la
vérification des systèmes temps réel
Responsable :
Mihaela Sighireanu (http://www.liafa.jussieu.fr/~sighirea)
Nature du stage :
Etude theorique
Nombre d'étudiants dans le groupe :
de 2 à 4.
Description du sujet :
Les systèmes temps réel sont les systèmes qui ont des contraintes
temporelles vis-à-vis de leur exécution. Par exemple, la durée d'une
activité ne peut excéder une certaine limite. Pour la modélisation de
ces systèmes on utilisent souvent des variables spéciales, nommées
horloges, qui enregistrent le temps écoulé depuis leur dernier mise à
zéro.
Pour la vérification des systèmes temps réel, les techniques
actuelles emploient plusieurs moyens de représentation de l'ensemble
d'états su système :
- Les DBM (Difference Bound Matrices) (voir la référence [4]) sont des
matrices (souvent creuses) qui sont indexées par les horloges
présentes dans le système. Dans l'élément correspondant aux horloges
x et y est stockée une paire (op, c) (où op in {<, <=} et c est une
constante) s'il existe une contrainte de la forme x-y op c. Les DBM
sont utilisées dans l'outil Kronos pour la vérification des systèmes
temporisés.
- Les CDD (Clock Difference Diagrams) (voir la référence [3]) combinent
les DBM et les diagrammes de décision binaire (BDD, voir référence
[1]). Un noeud dans un CDD correspond à l'appartenance de la
différence entre deux horloges à un intervalle de valeurs. Les CDD
sont utilisées dans l'outil UPAAL pour la vérification des systèmes
temporisés.
- Les DDD (Difference Decision Diagrams) (voir la référence [2]) sont
utilisées pour la représentation des formules booléennes sur des
inégalités de la forme x-y < c ou x-y <= c où les variables peuvent
être entières où réelles. Pour cela, elles adaptent le principe des
BDD (voir référence [1]) : en chaque noeud correspond à une
inégalité. Les DDD ont été utilisées pour la vérification de
plusieurs systèmes temps réel.
Le travail pour ce TER comporte deux aspects :
- Il faut lire et comprendre les articles donnés dans les références
qui présentent les trois structures de données.
- Il faut comprendre les différences (si elles existent) et les
avantages et les inconvénients de chaque structure.
Les conclusions de ce travail seront présentées sous forme d'un
exposé de 30 minutes.
Bibliographie
- R.E. Bryant. Symbolic Boolean Manipulation with Ordered Binary
Decision Diagrams, ACM Computing Surveys 24-3, September 1992.
- J. Myller, J. Lichtenberg, H. R. Andersen, and H. Hulgaard.
Difference Decision Diagrams. In proceedings Annual Conference of the
European Association for Computer Science Logic (CSL), September
20-25 1999. Madrid, Spain.
- K. G. Larsen, C. Weise and W. Yi, and J. Pearson. Clock Difference
Diagrams, Nordic Journal of Computing, 1999.
- S.Yovine. Model-checking timed automata. In Embedded Systems, G.
Rozenberg and F. Vaandrager eds., Lecture Notes in Computer Science,
1998.
Resultats :
- Ce sujet n'a ete jamais choisi :(