Publications

International journal papers

[TLR09] Louis-Marie Traonouez, Didier Lime and Olivier (H.) Roux. Parametric Model-Checking of Stopwatch Petri Nets.
In Journal of Universal Computer Science, 15(17):3273-3304, December 2009.
Abstract

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 model-checking 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.

Conference papers

International conferences
[TGJ+10] Louis-Marie Traonouez, Bartosz Grabiec, Claude Jard, Didier Lime and Olivier (H.) Roux. Symbolic Unfolding of Parametric Stopwatch Petri Nets.
8th International Symposium on Automated Technology for Verification and Analysis (ATVA 2010), September 2010, Singapore.
[GTJ+10] Bartosz Grabiec, Louis-Marie Traonouez, Claude Jard, Didier Lime and Olivier (H.) Roux. Diagnosis using unfoldings of parametric time petri nets.
8th International Conference on Formal Modelling and Analysis of Timed Systems (FORMATS 2010), September 2010, Vienna, Austria.
[LRST09] Didier Lime, Olivier (H.) Roux, Charlotte Seidner and Louis-Marie Traonouez. Romeo: A Parametric Model-Checker for Petri Nets with Stopwatches.
15th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2009), York, United Kingdom, March 2009.
[TLR08a] Louis-Marie Traonouez, Didier Lime and Olivier (H.) Roux. Parametric Model-Checking of Time Petri Nets with Stopwatches Using the State-Class Graph.
6th International Conference on on Formal Modelling and Analysis of Timed Systems (FORMATS 2008), Saint-Malo, France, September 2008.
[DSTR07] David Delfieu, Médésu Sogbohossou, Louis-Marie Traonouez and Sébastien Revol. Parametrized Study of a Time Petri Net.
4th International Conference on Cybernetics and Information Technologies, Systems and Applications (CITSA 2007), Orlando, Florida, USA, July 2008.
National conferences
[TDR07] Louis-Marie Traonouez, David Delfieu and 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, October 2007.

Book chapter

[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.
In Communicating Embedded Systems -- Software and Design, pages 165-225. ISTE Publishing / John Wiley, 2009.

Technical reports

[TLR08b] Louis-Marie Traonouez, Didier Lime and Olivier (H.) Roux. Parametric Model-Checking of Time Petri Nets with Stopwatches Using the State-Class Graph.
Technical Report RI2008_3, IRCCyN, September 2008. Extended version of [TLR08a].

Theses

[Tra09] Louis-Marie Traonouez. Vérification et dépliages de réseaux de Petri temporels paramétrés.
Ph.D thesis, University of Nantes, November 2009.
[Tra06b] Louis-Marie Traonouez. Stratégies d'analyse d'une fraction d'un réseau de Petri T-temporel
Master's thesis, École Centrale de Nantes, September 2006.
[Tra06a] Louis-Marie Traonouez. Raisonnement temporel en sémantique forte à partir de réseaux de Petri temporels exprimés en Logique Linéaire.
Master's bibliography report. École Centrale de Nantes, May 2006.