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/
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.
IMITATOR est un programme écrit en Python. Il est disponible ci-dessous.
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é.
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] |
[AACS09] | . 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] | . 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] | . An Inverse Method for Parametric Timed Automata. International Journal of Foundations of Computer Science 20(5), pages 819-836, 2009 ( PDF | BibTeX + Abstract ) |
[AEF09] | . 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] | . 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] | . 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] | . Automated Verification of a Parametric Real-Time Program: The ABR Conformance Protocol. In CAV '99, 1999. |
[CC04] | . The Octahedron Abstract Domain. In SAS'04, 2004. |
[CC05] | . Verification of Concurrent Systems with Parametric Delays Using Octahedra. In ACSD'05, 2005. |
[CEFX06] | . Verification of the Generic Architecture of a Memory Circuit Using Parametric Timed Automata. In FORMATS '06, 2006. |
[CS01] | . Parameterized Reachability Analysis of the IEEE 1394 Root Contention Protocol using TReX. In RT-TOOLS '01, 2001. |
[DKRT97] | . The Bounded Retransmission Protocol Must Be on Time!. In TACAS '97, 1997. |
[KNSW04] | . Symbolic Model Checking for Probabilistic Timed Automata. In FORMATS - FTRTFT'04, 2004. |
[NSY92] | . Compiling Real-Time Specifications into Extended Automata. In IEEE TSE, 1992. |