formal verification and synthesis for parametric timed systems


Roméo is a tool started by Olivier H. Roux in 2000, and developped since 2001 by Didier Lime (engine) and Olivier H. Roux (GUI) at École Centrale de Nantes and University of Nantes.

It allows the modelling of complex systems using extensions of time Petri nets. In particular, it features:

  • Parameter synthesis for the model-checking of a subset of the TCTL timed logic;
  • Joint parameter and controller synthesis;
  • Parameter synthesis for optimal reachability with an affine cost model.

Roméo is free and open source software licensed under the GPL compatible CeCILL license.


The latest version is 3.9.4 (2023-12-05), available as 64 bits binaries for:

The latest sources are also available.

Open Access logo PLoS transparent

The paper

Citing Roméo

Didier Lime, Olivier H. Roux, Charlotte Seidner, and Louis-Marie Traonouez. Romeo: A parametric model-checker for Petri nets with stopwatches. In Stefan Kowalewski and Anna Philippou, editors, 15th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2009), volume 5505 of Lecture Notes in Computer Science, pages 54-57, York, United Kingdom, March 2009. Springer.

        address = {York, United Kingdom},
        author = {Didier Lime and Olivier H. Roux and Charlotte Seidner and Louis-Marie Traonouez},
        editor = {Stefan Kowalewski and Anna Philippou},
        booktitle = {15th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2009)},
        month = mar,
        publisher = {Springer},
        series = {Lecture Notes in Computer Science},
        volume = {5505},
        pages = {54-57},
        title = {Romeo: A Parametric Model-Checker for {Petri} Nets with Stopwatches},
        year = 2009,

Some interesting problems modelled using Roméo

  • Analysis of resilience properties in oscillatory biological systems (Andreychenko et al.) Notice HAL ; En OpenAccess sur ScienceDirect.
  • Environment requirements for an aerial video tracking system (with Thales Research, Parquier et al.) ; en OpenAccess sur HAL
  • Operational scenarios modelling in the DGA OMOTESC project (with Sodius Nantes, Charlotte Seidner’s Ph. D.)
  • Analysis and optimisation of distributed software commissioning (Coullon et al.) ; en OpenAcess sur HAL.

A few related tools

Parameter synthesis for real-time systems

Verification of parametric timed automata

TIme petri Net Analyzer

Verification of time Petri nets


Verification of timed automata (and more)