The version of IMITATOR used to run the experiments is IMITATOR 2.8-alpha: build 1981; GitHub commit ab08ea8.
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|
Two sample PTAs designed specifically to illustrate parametric deadlock-freeness checking, and proposed in the manuscript.
This model is an asynchronous circuit made of an "AND" gate and an "OR" gate connected in a cyclic manner [CC05].
This is a toy example of a coffee machine from a Master course on verification of parametric systems.
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.
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].
This model is an asynchronous circuit made of a four components (logical gates or more complex components) connected together [CC04].
This is a toy example of a nuclear power plant from a Master course on verification of parametric systems.
This is a model of the Root Contention Protocol. Note that the model used is not exactly the one described in [CS01].
This is a model of a networked automation system, where several components communicate through an Ethernet bus [ACDFR09].
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.
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."
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