IMITATOR
Latest commit 44a20eb Sep 17, 2018
Permalink
Type Name Latest commit message Commit time
Failed to load latest commit information.
.travis Install extra latex fonts May 22, 2018
METAS Rename dir privatedoc into METAS Jul 10, 2015
benchmarks Modification to Train1PTA model May 16, 2018
bin replace uselessemptyfile.txt by .gitignore Apr 16, 2018
comparator Improve comparator Jun 1, 2018
doc Prepare release 2.10.4 Jul 2, 2018
logos Prepare 2.10 release Feb 21, 2018
scripts Move generate_HSC folder to the new HSC repository in the organization Apr 18, 2018
src Fix an issue for the distributed IMITATOR version (that did not compi… Sep 17, 2018
tests Update non-regression tests: add simple state spaces generations Jun 5, 2018
.gitignore Build documentation on travis CI May 22, 2018
.merlin test May 22, 2018
.travis.yml Build documentation on travis CI May 22, 2018
INSTALL.txt Installation instructions now point to IMITATOR Web site Oct 22, 2015
LICENSE
README.md Update description of IMITATOR Feb 22, 2017
RELEASES.md Prepare release 2.10.4 Jul 2, 2018
build-patator.sh a first possible refactoring for gen_imitator_distr.py Apr 10, 2018
build.sh a first possible refactoring for gen_imitator_distr.py Apr 10, 2018
build_number.txt
gen_build_info.py Replace printing multiple string by printing literal strings Apr 18, 2018
gen_imitator_distr.py a possible refactoring for gen_imitator_distr.py using regex Apr 10, 2018
gen_oasis.py a first possible refactoring for gen_imitator_distr.py Apr 10, 2018
gen_oasis_distr.py
incrementer.py a first possible refactoring for gen_imitator_distr.py Apr 10, 2018
interfaceCV.py Change extensions of generated files; fix a problem when the script i… Feb 20, 2017
oasis-config Update option in oasis tests Feb 8, 2017
oasis-config-distr Fix tests folder path May 22, 2018
oasis-unittestator-config Add basic unit testing for LinearConstraint Apr 30, 2016
paquito.yml Compiling is now non-distributed by default; for distributed installa… Jul 22, 2015
unittestator.sh

README.md

imitator

IMITATOR is an open source software tool to perform automated parameter synthesis for concurrent timed systems. IMITATOR takes as input a network of IMITATOR parametric timed automata (NIPTA): NIPTA are an extension of parametric timed automata [AHV93], a well-known formalism to specify and verify models of systems where timing constants can be replaced with parameters, i.e., unknown constants.

IMITATOR addresses several variants of the following problem: 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:

  • parametric safety and parametric reachability analysis [AHV93,JLR15],
  • parametric deadlock-freeness checking [Andre16],
  • cycle-existence synthesis,
  • cycle-existence synthesis under the non-Zenoness assumption [ANPS17],
  • the inverse method (also known as (robust) language or trace preservation synthesis) [ACEF09,AM15],
  • the behavioral cartography [AF10], and
  • parametric reachability preservation (PRP and PRPC) [ALNS15].

Numerous analysis options are available.

IMITATOR is able to run in a distributed fashion on a cluster (using the PRPC algorithm).

IMITATOR is mainly a command-line tool, but that can output results in graphical form. Furthermore, a graphical user interface is available in the CosyVerif platform.

IMITATOR was able to verify numerous case studies from the literature and from the industry, such as communication protocols, hardware asynchronous circuits, schedulability problems with uncertain periods and various other systems such as coffee machines (probably the most critical systems from a researcher point of view). Numerous benchmarks are available at the IMITATOR Web page, or on github.

For more info, please visit www.imitator.fr

Keywords

formal verification, model checking, software verification, parameter synthesis, parametric timed automata

References

[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.

[AFKS12] Étienne André, Laurent Fribourg, Ulrich Kühne and Romain Soulat. IMITATOR 2.5: A Tool for Analyzing Robustness in Scheduling Problems. In Dimitra Giannakopoulou and Dominique Méry (eds.), FM’12, LNCS 7436, Springer, pages 33–36, August 2012.

[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.

[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, May 2017. To appear.

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