IMITATOR

IMITATOR is an open source command-line model checker for parametric verification and robustness analysis of real-time systems. It performs automated parameter synthesis for concurrent timed systems described as networks of parametric timed automata extended with numerous features.

Keywords

formal verification, model checking, software verification, parameter synthesis, parametric timed automata, real-time systems, TCTL

Table of Contents

• Quick Start
• Installation
• Usage
• Examples and Benchmarks
• Documentation
• Build from Source
• Running Tests
• Features
• Contributing
• Citing IMITATOR
• License
• References

Quick Start

You can directly download a precompiled image from the GitHub releases page, and run it, for example:

bin/imitator benchmarks/example.imi

Alternatively, build IMITATOR locally and run the bundled example model:

git clone https://github.com/imitator-model-checker/imitator.git
cd imitator
.github/scripts/build.sh
bin/imitator benchmarks/example.imi

You can also build and run IMITATOR with Docker:

docker pull imitator/imitator
docker run --rm -v "$PWD:/workspace" imitator/imitator benchmarks/example.imi

Or build the image locally:

docker build -t imitator .
docker run --rm -v "$PWD:/workspace" imitator benchmarks/example.imi

Installation

In case of installation problems, please contact the developers via GitHub or imitator.fr.

The build helper supports Linux and macOS. It installs system dependencies, initializes an opam switch, installs the required OCaml libraries, and builds the executable:

.github/scripts/build.sh

After a successful build, the executable is available at:

bin/imitator

Usage

For most usages, IMITATOR takes an .imi model file and a .imiprop property file as inputs:

bin/imitator path/to/model.imi path/to/property.imiprop

For available command-line options, run:

bin/imitator -help

IMITATOR is mainly a command-line tool, but it can also output some results in graphical form when the relevant runtime tools are installed (typically dot).

Examples and Benchmarks

This repository includes a small example model in benchmarks/example.imi.

Additional case studies and benchmarks are available in the official IMITATOR benchmarks library and in related GitHub repositories. IMITATOR has been used on examples from the scientific literature and from the industry, including communication protocols, asynchronous hardware circuits, schedulability problems with uncertain periods, and other real-time systems.

For more information, visit imitator.fr.

Documentation

The repository contains several documentation entry points:

• Contribution guidelines
• Documentation overview
• User and developer manuals

Build from Source

IMITATOR is an OCaml project built with Dune. The project metadata is defined in dune-project, and the generated opam package file is IMITATOR.opam.

If your development environment is already configured, you can build directly with:

dune build

The recommended setup path for new contributors is still:

.github/scripts/build.sh

Running Tests

Run the Dune test target:

dune runtest

Run the regression test suite:

python tests/test.py

Before submitting OCaml changes, check formatting with:

scripts/format.sh --check

Features

IMITATOR takes as input a network of parametric timed automata [AHV93], a formalism for specifying and verifying systems where timing constants can be replaced with parameters, i.e., unknown constants. The input formalism can be seen as a subclass of parametric linear hybrid automata with constant clock rates, including stopwatches and multi-rate automata. IMITATOR supports many additions to parametric timed automata, including multi-rate clocks, linear constraints, global variables with simple or composite types (arrays, lists…), and user-defined functions.

IMITATOR addresses variants of the following question:

given a concurrent timed system, what are the values of the timing constants that guarantee that the model of the system satisfies some property?

Specifically, IMITATOR implements:

• parameter synthesis for a subset of TCTL, including safety, reachability, unavoidability, and their timed counterpart, such as $E \phi U_{[p; p+1)} \psi$ [AHV93] [JLR15],
• minimal-time and minimal-parameter reachability synthesis [ABPP19],
• parametric deadlock-freeness checking [Andre16],
• cycle-existence synthesis [NPP18] [AAPP21],
• cycle-existence synthesis under the non-Zenoness assumption [ANPS17],
• the inverse method, also known as robust language or trace preservation synthesis [ACEF09] [AS11] [AM15],
• behavioral cartography [AF10], and
• parametric reachability preservation (PRP and PRPC) [ALNS15].

Numerous analysis options are available. IMITATOR can also run in a distributed fashion on a cluster for the PRPC algorithm.

Contributing

Contributions are welcome. Please read CONTRIBUTING.md for the branching model, commit-message format, formatting command, test commands, and pull request checklist.

Citing IMITATOR

If you use IMITATOR in academic work, please cite it using the metadata in CITATION.cff, in particular:

Étienne André. IMITATOR 3: Synthesis of Timing Parameters Beyond Decidability. CAV 2021.

License

IMITATOR is distributed under the GPL-3.0-only license.

References

[AAPP21] Étienne André, Jaime Arias, Laure Petrucci and Jaco van de Pol. Iterative Bounded Synthesis for Efficient Cycle Detection in Parametric Timed Automata. In Jan Friso Groote and Kim G. Larsen (eds.), TACAS'21, Springer LNCS, April 2021.

[ABPP19] Étienne André, Vincent Bloemen, Laure Petrucci and Jaco van de Pol. Minimal-Time Synthesis for Parametric Timed Automata. In Tomas Vojnar and Lijun Zhang (eds.), TACAS'19, Springer LNCS, April 2019.

[ACEF09] Étienne André, Thomas Chatain, Emmanuelle Encrenaz and Laurent Fribourg. An Inverse Method for Parametric Timed Automata. International Journal of Foundations of Computer Science 20(5), pages 819-836, 2009.

[AF10] Étienne André and Laurent Fribourg. Behavioral Cartography of Timed Automata. In Antonín Kučera and Igor Potapov (eds.), RP'10, LNCS 6227, Springer, pages 76-90, September 2010.

[AHV93] Rajeev Alur, Thomas A. Henzinger and Moshe Y. Vardi. Parametric real-time reasoning. STOC'93, ACM, pages 592-601, 1993.

[ALNS15] Étienne André, Giuseppe Lipari, Nguyễn Hoàng Gia and Sun Youcheng. Reachability Preservation Based Parameter Synthesis for Timed Automata. In Klaus Havelund, Gerard Holzmann, Rajeev Joshi (eds.), NFM'15, LNCS 9058, Springer, pages 50-65, April 2015.

[AM15] Étienne André and Nicolas Markey. Language Preservation Problems in Parametric Timed Automata. In Sriram Sankaranarayanan and Enrico Vicario (eds.), FORMATS'15, Springer LNCS, September 2015.

[Andre16] Étienne André. Parametric Deadlock-Freeness Checking Timed Automata. In Augusto Cesar Alves Sampaio and Farn Wang (eds.), ICTAC'16, LNCS 9965, Springer, pages 469-478, October 2016.

[Andre21] Étienne André. IMITATOR 3: Synthesis of timing parameters beyond decidability. In Rustan Leino and Alexandra Silva (eds.), CAV'21, Springer LNCS 12759, pages 1-14, July 2021.

[ANPS17] Étienne André, Nguyễn Hoàng Gia, Laure Petrucci and Sun Jun. Parametric model checking timed automata under non-Zenoness assumption. In Clark Barrett and Temesghen Kahsai (eds.), NFM'17, Springer LNCS 10227, pages 35-51, May 2017.

[AS11] Étienne André and Romain Soulat. Synthesis of Timing Parameters Satisfying Safety Properties. RP 2011: 31-44, 2011.

[JLR15] Aleksandra Jovanovic, Didier Lime, Olivier H. Roux. Integer Parameter Synthesis for Real-Time Systems. IEEE Transactions on Software Engineering 41(5): 445-461, 2015.

[NPP18] Hoang Gia Nguyen, Laure Petrucci, Jaco van de Pol. Layered and Collecting NDFS with Subsumption for Parametric Timed Automata. ICECCS 2018: 1-9, 2018.