ROMEO

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.10.0 (2024-04-22), introducing Parametric DBMs, and available as 64 bits binaries for:

• Linux
• Mac OS X (still 3.9.4)
• Windows

The latest sources are also available.

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.

    @inproceedings{lime-TACAS-09,
        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,
    }

• 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.