IMITATOR

IMITATOR − Parameter synthesis for real-time systems

IMITATOR is a software tool for parametric verification and robustness analysis of real-time systems with parameters. It relies on the formalism of networks of parametric timed automata, augmented with integer variables and stopwatches.

IMITATOR implements the following algorithms:

Its extension to stopwatches (since IMITATOR 2.5) with clock updates allow its use in the framework of robust and parametric scheduling analysis of preemptive real-time systems [AFKS12].

IMITATOR is fully written in OCaml, and makes use of the Parma Polyhedra Library. It is available under the GNU General Public License.

Features

IMITATOR implements the following features:

Examples of graphical outputs

Trace set PTA export Trace set Behavioral cartography

The Team

IMITATOR has been initiated, and is still mainly developed, by Étienne André.

The following people contributed to IMITATOR.

Developers
Étienne André (2008– )
Camille Coti (2014)
Daphne Dussaud (2010)
Sami Evangelista (2014)
Ulrich Kühne (2010–2011)
Nguyễn Hoàng Gia (2014– )
Romain Soulat (2010–2013)
Compiling, packaging and external tools
Jaime Arias (2018–)
Corentin Guillevic (2015)
Sarah Hadbi (2015)
Jawher Jerray (2018–)
Fabrice Kordon (2015)
Alban Linard (2014–2015)
Sahar Mhiri (2018)
Moral support and suggestions by
Emmanuelle Encrenaz
Laurent Fribourg
Giuseppe Lipari

Credits

IMITATOR’s logo (the monkey on top of each page!) is a modifier version of KaterBegemot's Typing monkey.svg. Licence: Creative Commons Attribution-Share Alike 3.0 Unported.

Support

IMITATOR got support from the following institutions and projects.

Conferences on formal methods

Our list of conferences on formal methods