Adresse mail : dima
at univ-paris12 dot fr Les automates temporisés représentent un outil très puissant d'analyse et de vérification des systèmes temporisés. Mais le modèle se base sur une hypothèse parfois restrictive : celle du synchronisme des horloges. En effet, lorsque des systèmes distribués utilisent plusieurs horloges, celles-ci peuvent se désynchroniser au fil du temps, ce qui nécessite l'utilisation de divers protocôles de resynchronisation.
Le but de ce stage est d'étudier le modèle d'automates temporisés à horloges désynchronisées, en proposant des algorithmes efficaces de vérification. On chercherait ainsi à connaître la dérive maximale qui peut être envisagée entre les horloges sur un tel modèle, qui permet au modèle de satisfaire une certaine spécification donnée (par exemple, dans la logique Timed CTL).
Le travail demandé serait de modifier l'algorithme d'atteignabilité des automates temporisés, en incorporant l'hypothèse de l'existence d'une dérive paramétrique, et de synthétiser le max de cette dérive. L'algorithme sera à implémenter dans un outil de model-checking temporisé. Le point de départ c'est les articles [1] et [3] ci-dessous.
Références :
[1] C.
Dima : Dynamical
properties of timed automata revisited, Proceedings of FORMATS
2007, LNCS 4763, p. 130-146, 2007.
[2]
R: Alur, D. Dill, A theory of timed automata, Theor.
Comput. Sci. 126(2): 183-235 (1994) .
[3]
C. Daws, P. Kordy: Symbolic Robustness Analysis of Timed Automata.
FORMATS
2006: 143-155 .