Singe

IMITATOR

New! IMITATOR II and III available

This page is about the first (and outdated) version of IMITATOR (i.e., IMITATOR 1). The official page for all versions of IMITATOR is now:
http://www.lsv.ens-cachan.fr/Software/imitator/

Description

IMITATOR (standing for Inverse Method for Inferring Time AbstracT behaviOR) is an implementation of algorithm InverseMethod, described in [ACEF09].
It allows to generalize a concrete behavior of a Parametric Timed Automata, by synthesizing a constraint on the parameters.

This tool is being developed by Étienne André in collaboration with Laurent Fribourg and Emmanuelle Encrenaz.

Download

IMITATOR is a program written in Python. It is available below.

[IMITATOR.py]

Once Python and HyTech have been installed, IMITATOR can be applied to the file MyInputFile.hy using the following command :

> python IMITATOR.py MyInputFile

For any further information about the use of IMITATOR, please refer to the user manual [And09b].

For more information, please feel free to contact Étienne André.

Some Case Studies

Those case studies are summarized in [AEF09].

Name of the example	References	Input file	Log of the result
A toy example	[And09b]	[toyPTA.hy]	[toyPTA.log]
Flip-flop circuit	[CC04]	[flipflop.hy]	[flipflop.log]
"And-or" circuit	[CC05]	[AndOr.hy]	[AndOr.log]
Root Contention Protocol	[CS01]	[RCP.hy]	[RCP.log]
Bounded Retransmission Protocol	[DKRT97]	[brp.hy]	[brp.log]
CSMA/CD Protocol	[NSY92]	[csmacdNSY92.hy]	[csmacdNSY92.log]
CSMA/CD Protocol (Prism model)	[KNSW04]	[csmacdPrism.hy]	[csmacdPrism.log]
ABR conformance protocol	[BF99]	[ABR.hy]	[ABR.log]
Latch circuit studied in the framework of Valmem project	[AEF09]	[latchValmem.hy]	[latchValmem.log]
Portion of the SPSMALL Memory designed by ST-Microelectronics and studied in the framework of Valmem project	[CEFX06]	[spsmall.hy]	[spsmall.log]
Distributed control system studied in the framework of SIMOP project	[ACDFR09, AACS09]	[simop.hy]	[simop.log]

Talks

August 20th 2009 : IMITATOR: A Tool for Synthesizing Constraints on Timing Bounds of Timed Automata (ICTAC '09, Kuala Lumpur)
January 22nd 2010 : Synthesis of timing parameters in timed automata for the verification of hardware components (Séminaire MeFoSyLoMa, Paris)

References

[AACS09]	Saïd Amari, Étienne André, Thomas Chatain, Olivier De Smet, Bruno Denis, Emmanuelle Encrenaz, Laurent Fribourg and Sylvain Ruel. Timed Analysis of Networked Automation Systems Combining Simulation and Parametric Model Checking. Research report LSV-09-14, Laboratoire Spécification et Vérification, ENS Cachan, France, June 2009. SIMOP Research Report. 49 pages. ( PDF \| BibTeX + Abstract )
[ACDFR09]	Étienne André, Thomas Chatain, Olivier De Smet, Laurent Fribourg and Sylvain Ruel. Synthèse de contraintes temporisées pour une architecture d'automatisation en réseau. In Olivier H. Roux (ed.), MSR'09. Hermès, 2009. To appear. ( PDF \| BibTeX + Abstract )
[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 ( PDF \| BibTeX + Abstract )
[AEF09]	Étienne André, Emmanuelle Encrenaz and Laurent Fribourg. Synthesizing Parametric Constraints on Various Case Studies Using IMITATOR. Research report LSV-09-13, Laboratoire Spécification et Vérification, ENS Cachan, France, June 2009. 18 pages. ( PDF \| BibTeX + Abstract )
[And09]	Étienne André. IMITATOR: A Tool for Synthesizing Constraints on Timing Bounds of Timed Automata. In Martin Leucker and Carroll Morgan (eds.), ICTAC'09, LNCS. Springer, 2009 To appear. ( PDF \| BibTeX + Abstract )
[And09b]	Étienne André. Everything You Always Wanted to Know About IMITATOR (But Were Afraid to Ask). Research Report LSV-09-20, Laboratoire Spécification et Vérification, ENS Cachan, France, July 2009. 11 pages. ( PDF \| BibTeX + Abstract )
[BF99]	Béatrice Bérard, Laurent Fribourg. Automated Verification of a Parametric Real-Time Program: The ABR Conformance Protocol. In CAV '99, 1999.
[CC04]	Robert Clarisó, Jordi Cortadella. The Octahedron Abstract Domain. In SAS'04, 2004.
[CC05]	Robert Clarisó, Jordi Cortadella. Verification of Concurrent Systems with Parametric Delays Using Octahedra. In ACSD'05, 2005.
[CEFX06]	Remy Chevallier, Emmanuelle Encrenaz, Laurent Fribourg, Weiwen Xu. Verification of the Generic Architecture of a Memory Circuit Using Parametric Timed Automata. In FORMATS '06, 2006.
[CS01]	Aurore Collomb-Annichini, Mihaela Sighireanu. Parameterized Reachability Analysis of the IEEE 1394 Root Contention Protocol using TReX. In RT-TOOLS '01, 2001.
[DKRT97]	Pedro R. D’Argenio, Joost-Pieter Katoen, Theo C. Ruys, Jan Tretmans. The Bounded Retransmission Protocol Must Be on Time!. In TACAS '97, 1997.
[KNSW04]	Marta Kwiatkowska, Gethin Norman, Jeremy Sproston, Fuzhi Wang. Symbolic Model Checking for Probabilistic Timed Automata. In FORMATS - FTRTFT'04, 2004.
[NSY92]	X. Nicollin, Joseph Sifakis, Sergio Yovine. Compiling Real-Time Specifications into Extended Automata. In IEEE TSE, 1992.