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 (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.
IMITATOR implements the following features:
The user manual can be downloaded here. The downloading and installing instructions are available there.
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) |
| 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 | |
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.
IMITATOR got support from the following institutions and projects.
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 |
Our list of conferences on formal methods
