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 rational-valued global variables, stopwatches, multi-rate clocks, and some other useful features.

IMITATOR implements the following algorithms:

Its extension to stopwatches 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:

User manual

The user manual can be downloaded here. The downloading and installing instructions are available there.

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-…)
Vincent Bloemen (2018)
Jaime Arias (2018-…)
Camille Coti (2014)
Daphne Dussaud (2010)
Sami Evangelista (2014)
Ulrich Kühne (2010-2011)
Benjamin Loillier (2021-…)
Dylan Marinho (2021-…)
Nguyễn Hoàng Gia (2014-2017)
Laure Petrucci (2019-…)
Jaco van de Pol (2019-…)
Romain Soulat (2010-2013)
Compiling, packaging and external tools
Jaime Arias (2018-…)
Corentin Guillevic (2015)
Sarah Hadbi (2015)
Jawher Jerray (2018-2019)
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.

Version History

See RELEASES.md for a full list of changes in each version.

Version State space generation Inverse Method Variants of IM Cartography Graphical Output Stopwatches Arbitrary updates Distributed algorithms Reachability synthesis Property patterns Parametric deadlock checking Cycle synthesis Non-Zeno synthesis Optimal reachability Conditional updates Multi-rate automata
3.0 Yes Yes Yes Yes Yes Yes Yes Yes Yes Yes Yes Yes Yes Yes Yes Yes
2.12 Yes Yes Yes Yes Yes Yes Yes Yes Yes Yes Yes Yes Yes Yes Yes No
2.11 Yes Yes Yes Yes Yes Yes Yes Yes Yes Yes Yes Yes Yes Yes No No
2.10 Yes Yes Yes Yes Yes Yes Yes Yes Yes Yes Yes Yes Yes Yes No No
2.9 Yes Yes Yes Yes Yes Yes Yes Yes Yes Yes Yes Yes Yes No No No
2.8 Yes Yes Yes Yes Yes Yes Yes Yes Yes Yes Yes No No No No No
2.7 Yes Yes Yes Yes Yes Yes Yes Yes Yes Yes No No No No No No
2.6 Yes Yes Yes Yes Yes Yes Yes No Yes No No No No No No No
2.5 Yes Yes Yes Yes Yes Yes Yes No No No No No No No No No
2.4 Yes Yes Yes Yes Yes Yes No No No No No No No No No No
2.3 Yes Yes Yes Yes Yes No No No No No No No No No No No
2.0 to 2.2 Yes Yes No Yes Yes No No No No No No No No No No No
1.x No Yes No No No No No No No No No No No No No No

Conferences on formal methods

Our list of conferences on formal methods