Publications

Articles en revues internationales

[TLR09] Louis-Marie Traonouez, Didier Lime et Olivier (H.) Roux. Parametric Model-Checking of Stopwatch Petri Nets.
Dans Journal of Universal Computer Science, 15(17):3273-3304, décembre 2009.
Résumé

At the border between control and verification, parametric verification can be used to synthesize constraints on the parameters to ensure that a system verifies given specifications. In this paper we propose a new framework for the parametric verification of time Petri nets with stopwatches. We first introduce a parametric extension of time Petri nets with inhibitor arcs (ITPNs) with temporal parameters and we define a symbolic representation of the parametric state-space based on the classical state-class graph method. Then, we propose semi-algorithms for the parametric modelchecking of a subset of parametric TCTL formulae on ITPNs. These results have been implemented in the tool Romeo and we illustrate them in a case-study based on a scheduling problem.

Articles présentés en conférences

Conférences internationales
[TGJ+10] Louis-Marie Traonouez, Bartosz Grabiec, Claude Jard, Didier Lime and Olivier (H.) Roux. Symbolic Unfolding of Parametric Stopwatch Petri Nets.
8ème International Symposium on Automated Technology for Verification and Analysis (ATVA 2010), septembre 2010, Singapour.
[GTJ+10] Bartosz Grabiec, Louis-Marie Traonouez, Claude Jard, Didier Lime and Olivier (H.) Roux. Diagnosis using unfoldings of parametric time petri nets.
8ème International Conference on Formal Modelling and Analysis of Timed Systems (FORMATS 2010), septembre 2010, Vienne, Autriche.
[LRST09] Didier Lime, Olivier (H.) Roux, Charlotte Seidner et Louis-Marie Traonouez. Romeo: A Parametric Model-Checker for Petri Nets with Stopwatches.
15&eagrave;me International Conference on Tools and Algorithms for the Construction and Analysis of Systems, York, Royaume-Uni, mars 2009.
[TLR08a] Louis-Marie Traonouez, Didier Lime et Olivier (H.) Roux. Parametric Model-Checking of Time Petri Nets with Stopwatches Using the State-Class Graph.
6ème International Conference on on Formal Modelling and Analysis of Timed Systems (FORMATS 2008), Saint-Malo, France, septembre 2008.
[DSTR07] David Delfieu, Médésu Sogbohossou, Louis-Marie Traonouez et Sébastien Revol. Parametrized Study of a Time Petri Net.
4ème International Conference on Cybernetics and Information Technologies, Systems and Applications (CITSA 2007), Orlando, Floride, USA, juillet 2008.
Conférences francophones
[TDR07] Louis-Marie Traonouez, David Delfieu et Olivier (H.) Roux. Synthèse de contraintes de conception à partir de réseaux de Petri temporels paramétrés.
6ème Colloque Francophone sur la Modélisation des Systèmes Réactifs, (MSR'07), Lyon, France, octobre 2007.

Chapitre de livre

[JR09] A. David, G. Behrmann, P. Bulychev, T. Chatain, K.G. Larsen, P. Pettersson, J. Rasmussen, W. Yi, D. Lime, M. Magnin, O.H. Roux and L.M. Traonouez. Tools for Model-Checking Timed Systems.
Dans Communicating Embedded Systems -- Software and Design, pages 165-225. ISTE Publishing / John Wiley, 2009.

Rapports techniques

[TLR08b] Louis-Marie Traonouez, Didier Lime et Olivier (H.) Roux. Parametric Model-Checking of Time Petri Nets with Stopwatches Using the State-Class Graph.
Rapport technique RI2008_3, IRCCyN, septembre 2008. Version étendue de [TLR08a].

Mémoires

[Tra09] Louis-Marie Traonouez. Vérification et dépliages de réseaux de Petri temporels paramétrés.
Thèse de doctorat, Université de Nantes, novembre 2009.
[Tra06b] Louis-Marie Traonouez. Stratégies d'analyse d'une fraction d'un réseau de Petri T-temporel
Thèse de Master, École Centrale de Nantes, septembre 2006.
[Tra06a] Louis-Marie Traonouez. Raisonnement temporel en sémantique forte à partir de réseaux de Petri temporels exprimés en Logique Linéaire.
Rapport bibliographique de Master, École Centrale de Nantes, mai 2006.