formation par la recherche / formation doctorale / enseignement, stages / sujets de thèses

Axiomatisation des systèmes de transitions hiérarchiques

Localisation : Irisa, Rennes

Equipe Epatr

Responsable : Jean-Pierre Talpin (tél.: 0299847436, mail: Jean-Pierre.Talpin@irisa.fr)

Mot-clés : Systèmes mobiles synchrones et asynchrones, preuve de théorème.

Sujet : La spécification et la mise en uvre de systèmes réactifs distribués nécéssite la vérification de propriétés comportementales précises afin d'en assurer le fonctionnement correct et d'en garantir l'exécution efficace. Dans ce but, une théorie des systèmes de transitions synchrones a été élaborée. Cette structure possède une représentation canonique qui permet de mettre en évidence les propriétés d'endochronie et d'isochronie. Nous avons montré que cette structure pouvait être étendu afin de rendre compte de la mobilité et de comportements dynamiques [1]. L'objectif de la thèse sera d'étudier cette structure afin d'en proposer une axiomatisation à l'aide d'un assistant de preuve (e.g.  Coq, [2]). En utilisant cette axiomatisation, nous pourrons étudier la formalisation et la vérification de propriétés de programmes, comme par exemple: l'endochronie (équivalence entre observations synchrones et asynchrones), l'isochronie (équivalence entre compositions synchrones et asynchrones), la sécurité (l'accès légitime aux données d'un programme), le typage (l'accès correct aux données d'un programme). Mettant ce travail en perspective, nous pourrons enfin proposer une méthode générale mettant en uvre les techniques de démonstration automatique dans le cadre du déploiement distribué de composants applicatifs synchrones.

Bibliographie (disponible en http://www.irisa.fr/prive/talpin)

[1] J.-P. Talpin, A. Benveniste. Synchronous design and asynchronous deployment of mobile processes Research Report, in preparation. Inria, January 2000.

[2] Nowak, D., Beauvais, J.-R., Talpin, J.-P. Co-inductive axiomatization of a synchronous language International Conference on Theorem Proving in Higher-Order Logics. Springer Verlag, October 1998