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

Analyse sémantique des systèmes de transitions pré-ordre

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, interprétation abstraite.

Sujet : La spécification et la mise en uvre de systèmes réactifs nécéssite une analyse comportementale précise afin d'assurer la sureté de fonctionnement et de garantir l'exécution efficace. L'utilisation de langages de programmation synchrone facilitent la réalisation de systèmes critiques remplissant ces critères.

L'objectif de ce stage sera d'étudier la décision de propriétés de sureté (endochronie, accessibilité d'états, etc) dans les systèmes de transitions hiérarchiques [1] en ayant recours à des techniques d'interprétation abstraites [2].

Bibliographie

[1] J.-P. Talpin, A. Benveniste. and P. Le Guernic. Asynchronous deployment of synchronous transition systems. Research Report No. 1269. Irisa, October 1999.

[2] J.-P. Talpin, A. Benveniste., B. Caillaud and P. Le Guernic. Hierarchic normal forms for desynchronization. Research Report No. 3822. Inria, December 1999.

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

[4] "Timed polyhedra analysis for synchronous languages". Besson, F., Jensen, T., Talpin, J.-P. Static Analysis Symposium ( Sas'99). Springer Verlag Lectures Notes in Computer Science, September 1999.