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