• Accueil
• CV
• Publications
• 

	Louis-Marie Traonouez
	Post-Doctorant
	Adresse:	Software Technologies Laboratory Dipartimento di Sistemi e Informatica Università degli Studi di Firenze Via di Santa Marta 3 50145 Firenze (Italie)
	Email:

Présentation

Depuis novembre 2009 je travaille en tant que post-doctorant à l'Université de Florence en Italie, dans le Software Technologies Laboratory, sous la direction du professeur Enrico Vicario

De 2006 à 2009, j'ai réalisé mon doctorat en Automatique et Informatique Appliquée, à l' Université de Nantes, dans le laboratoire IRCCyN. J'ai travaillé pendant cette période dans l'équipe Systèmes Temps Réel avec Olivier (H.) Roux, David Delfieu et Didier Lime.

Actualités

Le 27 novembre 2009 j'ai soutenu ma thèse de doctorat à l'IRCCyN à Nantes. Le titre est :

"Vérification et dépliages de réseaux de Petri temporels paramétrés"

Le manuscrit de thèse et les transparents de la soutenance sont disponibles sur HAL ou bien ici.

Recherche

Thèmes: systèmes temps réel, vérification, réseaux de Petri temporels, model-checking, depliages, composition.

Je travail sur la vérification des systèmes temps réel. Plus précisément je m'intéresse aux méthodes de vérification formelles, à l'aide notamment des modèles de réseaux de Petri temporels et leurs extensions. Dans ce domaine, j'étudie les problématiques suivantes :

• L'extension de la technique de model-checking pour prendre en compte symboliquement des paramètres.
• Les méthodes de préservation de la concurrence telles que les dépliages.
• Les approches compositionnelles de modélisation et vérification.

Outils

Je participe au développement des outils suivants :

• Romeo, un outil pour la manipulation et l'analyse de réseaux de Petri temporels. Il permet l'édition et la simulation de réseaux de Petri temporels et performe des vérifications à la volée de propriétés temporelles. J'ai développé dans Romeo l'utilisation des paramètres temporels, notamment par model-checking paramétré, ainsi qu'un plugin de calcul de dépliages symboliques temporels.
• LLbox, un outil qui effectue des analyses temporelles de scenarios dans les réseaux de Petri temporels.