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.
|Nguyễn Hoàng Gia||(2014-2017)|
|Jaco van de Pol||(2019-…)|
|Compiling, packaging and external tools|
|Moral support and suggestions by|
IMITATOR got support from the following institutions and projects.