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.
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– ) |
| 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 and packaging | |
| Corentin Guillevic | (2015) |
| Sarah Hadbi | (2015) |
| Fabrice Kordon | (2015) |
| Alban Linard | (2014–2015) |
| 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
