IMITATOR

IMITATOR: Experiments Data for Infinity 2010

Case Studies Related to the Tool Paper on IMITATOR II (2010)

This page is dedicated to the case studies related to the manuscript IMITATOR II: A Tool for Solving the Good Parameters Problem in Timed Automata by Étienne André, published in the proceedings of the INFINITY’10 [Andre10infinity].

IMITATOR

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

These case studies were verified using IMITATOR 2.0 (standard inverse method).
To execute IMITATOR for these case studies, use:

	> ./IMITATOR case_study.imi case_study.pi0
Name of the example Reference Input File Reference Valuations Trace Set
"And-Or" Circuit [CC05] AndOr.imi AndOr.pi0 AndOr.gif
Bounded Retransmission Protocol brp.imi brp.pi0 brp.jpg
CSMA/CD Protocol (Prism model) csmacdPrism.imi csmacdPrism.pi0 csmacdPrism.jpg
Flip-flop circuit [CC07] flipflop.imi flipflop.pi0 flipflop.gif
Latch circuit studied in the framework of Valmem project [AEF09] latch.imi latch.pi0 latch.jpg
Root Contention Protocol RCP.imi RCP.pi0
Portion of the SPSMALL Memory designed by ST-Microelectronics and studied in the framework of Valmem project [CEFX09] spsmall.imi spsmall.pi0 spsmall.gif

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. (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]
[Andre10infinity]
Étienne André. IMITATOR II: A Tool for Solving the Good Parameters Problem in Timed Automata. In Yu-Fang Chen and Ahmed Rezine (eds.), INFINITY’10, Electronic Proceedings in Theoretical Computer Science 39, pages 91–99, 2010. Creative Commons Attribution 3.0 Unported (CC BY 3.0) (English) [PDF (published version) | BibTeX | Slides]
[CC05]
Robert Clarisó, Jordi Cortadella. Verification of Concurrent Systems with Parametric Delays Using Octahedra. In ACSD’05, 2005.
[CC07]
Robert Clarisó, Jordi Cortadella. The Octahedron Abstract Domain. In Science of Computer Programming 64(1), pages 115-139, 2007.
[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.

Contact

Étienne André