IMITATOR

IMITATOR: Experiments Data of IMITATOR 1.0

Case Studies Related to IMITATOR 1 (2009)

Singe

This page is dedicated to the case studies related to the very first version of IMITATOR (that used to consist in a Python script calling HyTech).

IMITATOR

The version of IMITATOR used to run the experiments is IMITATOR 1.3.

These case studies were verified using IMITATOR 1.3 (standard inverse method).
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 [Andre09manual].

Case Studies

Those case studies are summarized in [AEF09].

Name of the example Reference Input File Log and result
A toy example [Andre09manual] [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) [KNSW07] [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 [CEFX09] [spsmall.hy] [spsmall.log]
Distributed control system studied in the framework of SIMOP project [ACDFR09] [simop.hy] [simop.log]

References

[ACDFR09]
Étienne André, Thomas Chatain, Olivier De Smet, Laurent Fribourg and Silvain Ruel. Synthèse de contraintes temporisées pour une architecture d’automatisation en réseau. In Didier Lime and Olivier H. Roux (eds.), MSR’09, Journal Européen des Systèmes Automatisés 43(7-9), Hermès, pages 1049–1064, 2009.
[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. (English) [PDF (published version) | PDF (author version) | BibTeX]
[AEF09]
Étienne André. 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]
[Andre09ictac]
Étienne André. IMITATOR: A Tool for Synthesizing Constraints on Timing Bounds of Timed Automata. In Martin Leucker and Carroll Morgan (eds.), ICTAC’09, LNCS 5684, Springer, pages 336–342, August 2009. [PDF (published version) | PDF (author version) | BibTeX | Slides]
[Andre09manual]
É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. [PDF | BibTeX + Abstract]
[BF99]
Béatrice Bérard and Laurent Fribourg. Automated Verification of a Parametric Real-Time Program: The ABR Conformance Protocol. In CAV’99, 1999.
[CC04]
Robert Clarisó, Jordi Cortadella. Verification of timed circuits with symbolic delays. In ASP-DAC 2004: 628-633, 2004.
[CC05]
Robert Clarisó, Jordi Cortadella. Verification of Concurrent Systems with Parametric Delays Using Octahedra. In ACSD’05, 2005.
[CEFX09]
Rémy Chevallier, Emmanuelle Encrenaz-Tiphène, Laurent Fribourg, and Weiwen Xu. Timed verification of the generic architecture of a memory circuit using parametric timed automata. Formal Methods in System Design, 34(1):59–81, 2009.
[CS01]
Aurore Collomb-Annichini and Mihaela Sighireanu. Parameterized Reachability Analysis of the IEEE 1394 Root Contention Protocol using TReX. In Proceedings of the Real-Time Tools Workshop (RT-TOOLS’2001).
[DKRT97]
Pedro R. D’Argenio, Joost-Pieter Katoen, Theo C. Ruys, Jan Tretmans: The Bounded Retransmission Protocol Must Be on Time! TACAS 1997: 416-431.
[KNSW07]
Marta Kwiatkowska, Gethin Norman, Jeremy Sproston, and Fuzhi Wang. Symbolic Model Checking for Probabilistic Timed Automata. Information and Computation, 205(7), pages 1027-1077. July 2007.
[NSY92]
X. Nicollin, Joseph Sifakis, Sergio Yovine. Compiling Real-Time Specifications into Extended Automata. In IEEE Transations on Software Engineering. 1992.

Contact

Étienne André