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:
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.
Our list of conferences on formal methods
