Roméo

Roméo: formal verification and synthesis for timed systems

About

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:

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

Download

The latest version is 3.8.0 (2020-07-13), available as 64 bits binaries for:

The latest sources are also available.

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.

    @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,
    }

Some interesting problems modelled using Roméo

A few related tools