This page is dedicated to the case studies related to the manuscript Parametric model checking timed automata under non-Zenoness assumption by Étienne André, Hoang Gia Nguyen, Laure Petrucci and Jun Sun, published in the proceedings of the NFM’17 [ANPS17].
The version of IMITATOR used to run the experiments is IMITATOR 2.8.1-working (branch learning, build 2108, GitHub hash 3ca9b1ca7cab3271e82d852a72c922665e9b02c7).
We present in the following table a list of case studies computed using various algorithms using IMITATOR.
The model can be obtained by clicking on the case study name; the rectangular parameter domain can be obtained by clicking on the number of integer points (|V| column); logs including results can be obtained by clicking on the response time of each algorithm; a graphical representation can be obtained by clicking on the [g] (when available).
Benchmark | SynthCycle | CUBdetect + SynthNZ | CUBtrans + SynthNZ | |||||||||||||||
---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|
Name | Ref | |A| | |X| | |P| | |L| | t (s) | Result | Approximation? | detection t (s) | Total t (s) | CUB for | Result | Approximation? | transformation t (s) | Total t (s) | |L CUB| | Result | Approximation? |
CSMA/CD | [KNSW07] | 3 | 3 | 3 | 28 | 3600 | true | invalid | 0.013 | 0.013 | false | - | - | 0.3 | 3600 | 74 | true | exact |
Fischer | [AHV93] | 3 | 2 | 4 | 13 | 3600 | true | invalid | 0.003 | 0.003 | false | - | - | 0.012 | 3600 | 20 | true | exact |
RCP | 5 | 6 | 5 | 48 | 3600 | some | invalid | 0.013 | 0.013 | false | - | - | 0.348 | 3600 | 71 | false | under-approximation | |
WFAS | [BBLS15] | 3 | 4 | 2 | 10 | 3600 | some | invalid | 0.009 | 0.009 | false | - | - | 0.246 | 1848 | 40 | some | exact |
AndOr | [CC05] | 4 | 4 | 4 | 27 | 3600 | some | invalid | 0.012 | 0.012 | false | - | - | 0.059 | 3600 | 34 | some | under-approximation |
Flip-flop | [CC04] | 5 | 5 | 2 | 52 | 0.058 | false | exact | 0.002 | 0.086 | true | false | exact | 0.01 | 0.972 | 58 | false | exact |
Sched5 | 12 | 21 | 2 | 153 | 190 | false | exact | 0.051 | 0.051 | false | - | - | 1.18 | 3600 | 180 | false | under-approximation | |
simop | [ACDFR09] | 5 | 8 | 2 | 46 | 3600 | false | invalid | 0.012 | 0.012 | false | - | - | 0.219 | 3600 | 81 | false | under-approximation |
train-gate | 4 | 5 | 9 | 11 | 3600 | false | invalid | 0 | 3600 | some | false | under-approximation | 0.059 | 3600 | 23 | false | under-approximation | |
coffee | 3 | 2 | 3 | 4 | 3600 | some | invalid | 0 | 3600 | some | some | under-approximation | 0.012 | 3600 | 10 | some | under-approximation | |
CUBPTA1 | 3 | 1 | 3 | 2 | 0.006 | true | over-approximation | 0 | 0.015 | some | some | under-approximation | 0.006 | 0.073 | 6 | some | exact | |
JLR15 | [JLR15] | 3 | 2 | 2 | 2 | 3600 | false | invalid | 0 | 3600 | true | false | under-approximation | 0 | 3600 | 3 | false | under-approximation |
This is a model of the CSMA/CD proposed in [KNSW07] and modeled for the PRISM model checker. The version we consider replaces probabilities with non-determinism.
This is a model of Fischer’s mutual exclusion protocol proposed in [AHV93].
This is a model of IEEE 1394 Root Contention Protocol.
This is a model of a wireless fire alarm system studied in [BBLS15].
This small asynchronous circuit consists in an AND gate connected to an OR gate in a cyclic manner; its behavior is studied in [CC05].
This asynchronous circuit consists of several gates connected to each other in a cyclic manner; its behavior is studied in [CC04].
This is the model of the schedulability of 5 fixed-priority tasks in a single processor.
This is a model of a networked automation system studied in [ACDFR09].
This is a model of a train-gate-controller from here.
This is a model of a simple coffee machine used as a teaching example.
This is a toy case study to illustrate and test CUB-PTAs.
This is a case study studied in [JLR15].
For all case studies, the following commands were used:
> IMITATOR case_study.imi case_study.v0 -mode EF -merge -output-cart
> IMITATOR case_study.imi case_study.v0 -mode cover -merge -output-cart
> IMITATOR case_study.imi case_study.v0 -mode cover -EFIM -merge -output-cart