IMITATOR

IMITATOR: Experiments Data for ICTAC 2016

Case Studies Related to Parametric Deadlock-Freeness Checking Timed Automata

IMITATOR

The version of IMITATOR used to run the experiments is IMITATOR 2.8-alpha: build 1981; GitHub commit ab08ea8.

Download

Case studies

We present in the following table a list of case studies to which PDFC was applied.

The IMITATOR input model as a network of IMITATOR PTAs (IPTAs) can be obtained by clicking on the case study name; a graphical representation of the model is also available; the result is obtained by clicking on the constraint ("K") column; the textual description of all explored states is obtained by clicking on the number of states. A graphical representation of the state space or of the computed constraint (projected onto 2 parameter dimensions, hence not always meaningful) can also be obtained by clicking on the [g], when available.

Case study Model Graphics Ref |A| |X| |P| States Time K Soundness Full log
Fig1.a PDFC4.imi PDFC4-pta.jpg 1 1 2 3 [g] 0.012 s NNCC [g] exact log
Fig1.b PDFC6.imi PDFC6-pta.jpg 1 1 1 2 [g] 0.005 s False exact log
And–Or AndOr.imi AndOr-pta.jpg [CC05] 4 4 4 5265 time out [NNCC , NNCC] Under/over-approximation log
Coffee machine 1 coffee.imi coffee-pta.jpg 1 2 3 9042 time out [NNCC , NNCC] Under/over-approximation log
Coffee machine 2 coffeeDrinker-toolpaper.imi coffeeDrinker-toolpaper-pta.jpg 2 3 3 51 [g] 0.198 s NNCC [g] exact log
CSMA/CD csmacdPrism.imi csmacdPrism-pta.jpg [KNSW07] 3 3 3 38 [g] 0.105 s False exact log
Flip-flop flipflop.imi flipflop-pta.jpg [CC04] 6 5 2 20 [g] 0.093 s False exact log
Nuclear plant NuclearPlant.imi NuclearPlant-pta.jpg 1 2 4 13 [g] 0.014 s NNCC [g] exact log
Root Contention Protocol RCP.imi RCP-pta.jpg [CS01] 5 6 5 2091 [g] 10.631 s False exact log
SIMOP simop.imi simop-pta.jpg [ACDFR09] 5 8 2 22894 [g] time out NNCC over-approximation log
Train1PTA Train1PTA.imi Train1PTA-pta.jpg 1 2 3 11 [g] 0.025 s NNCC [g] exact log
WFAS WFAS-BBLS15-det.imi WFAS-BBLS15-det-pta.jpg [BBLS15] 3 4 2 14614 time out [NNCC , NNCC] Under/over-approximation log

Description of the Case Studies

Figs 1.a and 1.b

Two sample PTAs designed specifically to illustrate parametric deadlock-freeness checking, and proposed in the manuscript.

And–Or circuit

This model is an asynchronous circuit made of an "AND" gate and an "OR" gate connected in a cyclic manner [CC05].

Coffee machine 1

This is a toy example of a coffee machine from a Master course on verification of parametric systems.

Coffee machine 2

This is an example of a PTA modeling a coffee machine together with a second PTA modeling a researcher drinking coffee. This benchmark is used to introduce the features of IMITATOR.

CSMA/CD Protocol

This is the Carrier sense multiple access with collision detection protocol modeled as a network of PTAs. This model is the non-probabilistic version from the PRISM model checker [KNSW07].

Flip-flop circuit

This model is an asynchronous circuit made of a four components (logical gates or more complex components) connected together [CC04].

Nuclear Plant

This is a toy example of a nuclear power plant from a Master course on verification of parametric systems.

Root Contention Protocol

This is a model of the Root Contention Protocol. Note that the model used is not exactly the one described in [CS01].

SIMOP

This is a model of a networked automation system, where several components communicate through an Ethernet bus [ACDFR09].

Train

This is a toy example of a classical train/gate/controller system used in tutorials on IMITATOR as well as in a Master course on verification of parametric systems.

WFAS

This is a wireless fire alarm system modelled as a PTA and described in [BBLS15]. As written in [BBLS15], "in the alarm setup, a number of wireless sensors communicate with the alarm controller over a limited number of communication channels (in our simplified example we assume just a single channel). The wireless alarm system uses a variant of Time Division Multiple Access (TDMA) protocol in order to guarantee a safe communication of multiple sensors over a shared communication channel. In TDMA the data stream is divided into frames and each frame consists of a number of time slots allocated for exclusive use by the present wireless sensors. Each sensor is assigned a single slot in each frame where it can transmit on the shared channel."

Calling IMITATOR

For all case studies, the following command is used:

> ./imitator case_study.imi -mode PDFC -output-states -output-trace-set -output-cart -output-result -time-limit 300

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.
[BBLS15]
Nikola Beneš, Peter Bezděk, Kim Guldstrand Larsen, Jirí Srba: Language Emptiness of Continuous-Time Parametric Timed Automata. In ICALP 2015, Part II, volume 9135 of LNCS, pages 69-81. Springer, 2015.
[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.
[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).
[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.

Contact

Étienne André