Titre

Analyses de systèmes hybrides

Encadrants

Étienne André & Laurent Fribourg
Tél: 01 47 40 22 68 & 01 47 40 75 36
Web: http://www.lsv.ens-cachan.fr/~andre & Web: http://www.lsv.ens-cachan.fr/~fribourg
Email: andre@lsv.ens-cachan.fr & fribourg@lsv.ens-cachan.fr
Laboratoire Spécification et Vérification
École Normale Supérieure de Cachan
61, avenue du Président Wilson
94235 Cachan CEDEX

Contexte

Ce stage s’inscrit dans le cadre de la vérification de systèmes temporisés, à l’aide d’automates temporisés [AD94]. Cette extension des automates d’états finis permet d’utiliser des horloges, ou variables évoluant linéairement dans le temps à la même vitesse. Ces automates temporisés permettent notamment la vérification de matériel (circuits mémoires, etc.), ou encore de protocoles de communication. L’utilisation d’automates temporisés est cependant coûteuse en terme de performances, car le nombre d’états accessibles explose rapidement.

Un algorithme, la méthode inverse [ACEF09], permet de contourner cette explosion, et de vérifier des systèmes plus grands qu’avec d’autres méthodes classiques. Une implémentation, Imitator [And09, And], a été réalisée.

Descriptif du stage

Nous envisageons l’extension de cette méthode aux automates hybrides [ACH+95]. Cette extension des automates temporisés diffère de ceux-ci par le fait que les horloges peuvent désormais évoluer avec des vitesses différentes.

Après une initiation aux automates temporisés et à la méthode inverse, le stage s’articulera autour de ces deux axes :

• Extension de la méthode inverse aux automates hybrides, en collaboration avec les membres de l’équipe ;
• Implémentation d’un prototype pour cette extension.

Prérequis

Ce stage s’adresse à un étudiant de Licence 3 ou Master 1, qui est intéressé par une initiation aux thématiques d’une équipe de recherche. Les étudiants d’écoles d’ingénieurs sont les bienvenus.

Il conviendra de connaître au moins un langage d’implémentation ; une connaissance d’OCaml serait un plus.

Conditions du stage

Le stage se déroule au LSV (Laboratoire Spécification et Vérification) à l’ENS Cachan.

Le stage devra durer au moins 8 semaines. Le stage est prévu pour se dérouler durant l’été 2010, mais d’autres périodes sont également envisageables en fonction des disponibilités de l’étudiant.

Références

[ACEF09]

É. André, T. Chatain, E. Encrenaz, and L. Fribourg. An inverse method for parametric timed automata. International Journal of Foundations of Computer Science, 20(5):819–836, October 2009.

[ACH⁺95]

R. Alur, C. Courcoubetis, N. Halbwachs, T.A. Henzinger, P.-H. Ho, X. Nicollin, A. Olivero, J. Sifakis, and S. Yovine. The algorithmic analysis of hybrid systems. Theoretical Computer Science, 138:3–34, 1995.

[AD94]

R. Alur and D. L. Dill. A theory of timed automata. TCS, 126(2):183–235, 1994.

[And]

Étienne André. Imitator web page. http://www.lsv.ens-cachan.fr/~andre/IMITATOR.

[And09]

Étienne André. IMITATOR: A tool for synthesizing constraints on timing bounds of timed automata. In Martin Leucker and Carroll Morgan, editors, ICTAC’09, volume 5684 of Lecture Notes in Computer Science, pages 336–342. Springer, 2009.

Ce document a été traduit de L^AT_EX par H^EV^EA