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 (pour Inverse Method for Inferring Time AbstracT behaviOR) est une implémentation de l’algorithme InverseMethod, décrit dans [ACEF09].
Il généralise le comportement des automates temporisés paramétrés en synthétisant une contrainte sur les paramètres.

Cet outil est développé par Étienne André en collaboration avec Laurent Fribourg et Emmanuelle Encrenaz.

Téléchargement

IMITATOR est un programme écrit en Python. Il est disponible ci-dessous.

[IMITATOR.py]

Une fois Python et HyTech installés, IMITATOR peut être appliqué au fichier MyInputFile.hy en exécutant la commande suivante :

> python IMITATOR.py MyInputFile

Pour plus d’information sur l’utilisation d’IMITATOR, reportez-vous au manuel utilisateur [And09b].

Pour toute information, n’hésitez pas à contacter Étienne André.

Quelques études de cas

Ces études de cas sont synthétisées dans [AEF09].

Nom de l’exemple Références Fichier d’entrée Trace du résultat
Un exemple jouet [And09b] [toyPTA.hy] [toyPTA.log]
Circuit flip-flop [CC04] [flipflop.hy] [flipflop.log]
Circuit « and-or » [CC05] [AndOr.hy] [AndOr.log]
Root Contention Protocol [CS01] [RCP.hy] [RCP.log]
Bounded Retransmission Protocol [DKRT97] [brp.hy] [brp.log]
Protocole CSMA/CD [NSY92] [csmacdNSY92.hy] [csmacdNSY92.log]
Protocole CSMA/CD (modèle Prism) [KNSW04] [csmacdPrism.hy] [csmacdPrism.log]
Protocole ABR [BF99] [ABR.hy] [ABR.log]
Circuit bascule « latch » étudié dans le cadre du projet Valmem [AEF09] [latchValmem.hy] [latchValmem.log]
Portion de la mémoire SPSMALL créée par ST-Microelectronics et étudiée dans le cadre du projet Valmem [CEFX06] [spsmall.hy] [spsmall.log]
Système de contrôle distribué étudié dans le cadre du projet SIMOP [ACDFR09, AACS09] [simop.hy] [simop.log]

Présentations

Références

[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. Rapport de recherche 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. Rapport de recherche 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.

Valid XHTML 1.0 Strict