This page is dedicated to the case studies related to the submitted paper "Merge and Conquer: State Merging in Parametric Timed Automata".

The version of IMITATOR used to compute the case studies is **IMITATOR 2.6.1**.

It can be downloaded from the download page.

We present in the following table a list of case studies computed using the inverse method using the above implementation of IMITATOR.

We give from left to right the name of the case study (with a link to the IMITATOR model), the reference, the reference valuation file pi0, the number |A| of automata in parallel, the number |X| of clocks, the number |P| of parameters, and for each of the 2 algorithms, the number |S| of states computed, the number |T| of transitions computed, the computation time t in seconds (excluding the generation of the graphical outputs), and whether the result is complete or maybe not complete. In the last 3 columns, we compare the results: first, we divide the number of states in IM by the number of states in IMMerge' and multiply by 100 (hence, a number smaller than 100 denotes an improvement of IMMerge'); second, we perform the same comparison for the computation time; the last column indicates whether K = Kmerge' or K ⊂ Kmerge'.

Experiments were performed on a KUbuntu 12.10 64 bits system running on an Intel Core i7 CPU 2.67GHz with 4 GiB of RAM.

Case study | Reference | Pi0 | |X| | |P| | IM | IMMerge' | Comparison | ||||||||||
---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|

|S| | |T| | t | Complete | Result | |S| | |T| | t | Complete | Result | States | time | K | |||||

And-Or | [CC05] | AndOr.pi0 | 4 | 12 | 11 | 11 | 0.052 s | Yes | log – states – traces | 9 | 9 | 0.056 s | Yes | log – states – trace set | 82 | 108 | = |

Flip-Flop | [CC07] | flipflop.pi0 | 5 | 12 | 11 | 10 | 0.06 s | Yes | log – states – traces | 9 | 9 | 0.057 s | Yes | log – states – trace set | 82 | 95 | = |

Latch | [Andre10] | latchValmem.pi0 | 8 | 13 | 18 | 17 | 0.083 s | ? | log – states – traces | 12 | 12 | 0.069 s | ? | log – states – trace set | 67 | 83 | = |

SPSMALL memory | [AS13] | spsmall.pi0 | 10 | 26 | 31 | 30 | 0.618 s | Yes | log – states – traces | 31 | 30 | 0.613 s | Yes | log – states – trace set | 100 | 99 | = |

SIMOP | [AS13] | simop.pi0 | 8 | 7 | - | - | Out of memory | - | - | 172 | 262 | 2.52 s | ? | log – states – trace set | 0 | 0 | - |

BRP | [DKRT97] | brp.pi0 | 7 | 6 | 429 | 474 | 3.5 s | Yes | log – states – traces | 426 | 473 | 4.3 s | Yes | log – states – trace set | 99 | 123 | = |

CSMA/CD bc2 | [KNSW07] | csmacdPrism.pi0 | 3 | 3 | 301 | 462 | 0.514 s | Yes | log – states – traces | 300 | 461 | 0.574 s | Yes | log – states – trace set | 100 | 112 | = |

CSMA/CD bc6 | [KNSW07] | csmacdPrism6.pi0 | 3 | 3 | 13365 | 14271 | 18.3 s | Yes | log – states – traces | 13365 | 14271 | 25.4 s | Yes | log – states – trace set | 100 | 139 | = |

RCP | [HRSV02] | RCP.pi0 | 5 | 6 | 327 | 518 | 0.748 s | Yes | log – states – traces | 115 | 186 | 0.684 s | Yes | log – states – trace set | 35 | 91 | = |

WLAN | [KNS02] | wlan.pi0 | 2 | 8 | - | - | Out of memory | - | - | 8430 | 15152 | 2137 s | Yes | log – states – trace set | 0 | 0 | - |

ABT | [FLMS12] | astrium_basic_thermal_fp.pi0 | 7 | 7 | 63 | 62 | 0.344 s | ? | log – states – traces | 63 | 62 | 0.335 s | ? | log – states – trace set | 100 | 97 | = |

AM02 | [AM02] | am02.pi0 | 3 | 4 | 182 | 215 | 0.369 s | Yes | log – states – traces | 53 | 70 | 0.112 s | Yes | log – states – trace set | 29 | 30 | ⊂ |

BB04 | [BB04] | bb.pi0 | 6 | 7 | 806 | 827 | 28 s | ? | log – states – traces | 141 | 145 | 3.15 s | ? | log – states – trace set | 17 | 11 | = |

CTC | [???] | concurent_tasks_chain.pi0 | 15 | 21 | 1364 | 1363 | 88.9 s | Yes | log – states – traces | 215 | 264 | 17.6 s | Yes | log – states – trace set | 16 | 20 | = |

LA02 | [Tamura07] | LA02_2.pi0 | 3 | 5 | 6290 | 8023 | 751 s | ? | log – states – traces | 383 | 533 | 17.7 s | Yes | log – states – trace set | 6 | 2 | ⊂ |

LPPRC10 | [LPPRC10] | hppr10_audio.pi0 | 4 | 7 | 78 | 102 | 0.39 s | ? | log – states – traces | 31 | 40 | 0.251 s | ? | log – states – trace set | 40 | 64 | = |

M2.4 | [AAM06] | maler_2_4.pi0 | 3 | 8 | 1497 | 1844 | 8.89 s | Yes | log – states – traces | 119 | 181 | 0.374 s | Yes | log – states – trace set | 8 | 4 | ⊂ |

The AndOr case study consists in an "AND" gate linked to an "OR" gate in a cyclic manner.

The flip-flop case study consists in a flip-flop circuit made of 4 components.

The latch case study is a sery of gates simulating the behavior of a latch, designed by ST-Microelectronics during a joint project with LSV.

The SPSMALL case study is the model of an abstraction of an asynchronous circuit designed and sold by ST-Microelectronics.

This case study is a networked automation system studies in the framework of the SIMOP project (LSV and LURPA, ENS de Cachan, France).

BRP is the bounded retransmission protocol.

The 2 CSMA/CD models correspond to the non-probabilistic version of the model described in [KNSW07]. The differences between our two versions is the value of the maximum backoff (2 and 6 respectively).

RCP is the root contention protocol of the IEEE 1394 (“FireWire”) High Performance Serial Bus, considered in the parametric framework in [HRSV02].

WLAN corresponds to the IEEE 802.11 Wireless Local Area Network Protocol.

The ABT case study is a problem of scheduling 3 periodic tasks on a single processor studied in the setting of a collaboration between Astrium and LSV.

The AM02 case study is a problem of preemptive job-shop scheduling with two jobs on three machines.

The BB04 case study corresponds to a three task example from [BB04, Section III, table 1]. It is an FP scheduling problem with three cyclic tasks on one machine.

The CTC (concurrent task chain) case study does not use cyclic tasks but instead has a 4 task chain and a concurrent 3 task chain. Each task in a chain cannot start until the previous one has not terminated. Each task in each chain has a given fixed priority. A scheduler assigns which task has the computational time with a FP policy.

The **LPPRC10** is a two-cyclic-tasks problem with an EDF scheduler.

The M2.4 case study is a problem of non-preemptive scheduling. Two sequences of tasks have to run concurrently trough 4 machines. The goal is to schedule the tasks to meet the deadline on the overall execution time.

For all case studies, the standard inverse method IM was called using the following options:

> IMITATOR case_study.imi case_study.pi0 -with-dot -with-log

For all case studies, the inverse method with merging IMMerge' was called using the following options:

> IMITATOR case_study.imi case_study.pi0 -merge -with-dot -with-log

- [AAM06]
- Yasmina Abdeddaïm, Eugene Asarin, and Oded Maler.
*Scheduling with timed automata*. In Theoretical Computer Science 354(2), pages 272–300, 2006. - [AM02]
- Yasmina Abdeddaïm and Oded Maler.
*Preemptive job-shop scheduling using stopwatch automata*. In TACAS'02, pages 113–126, 2002. - [Andre10]
- Étienne André. An Inverse Method for the Synthesis of Timing Parameters in Concurrent Systems. Ph.D. thesis, Laboratoire Spécification et Vérification, ENS Cachan, France, December 2010.
- [AS13]
- Étienne André and Romain Soulat. The Inverse Method. ISTE Ltd and John Wiley & Sons Inc., 2013.
- [BB04]
- Enrico Bini and Giorgio C. Buttazzo.
*Schedulability analysis of periodic fixed priority systems*. IEEE Trans. Computers, 53(11):1462–1473, 2004. - [CC05]
- Robert Clarisó, Jordi Cortadella.
*Verification of Concurrent Systems with Parametric Delays Using Octahedra*. In ACSD’05, 2005. - [CC07]
- Robert Clarisó, Jordi Cortadella.
*The Octahedron Abstract Domain*. In Science of Computer Programming 64(1), pages 115-139, 2007. - [DKRT97]
- P.R. D’Argenio, J.P. Katoen, T.C. Ruys, and G.J. Tretmans.
*The bounded retransmission protocol must be on time!*. In TACAS’97. - [FLMS12]
- Laurent Fribourg, David Lesens, Pierre Moro, and Romain Soulat.
*Robustness Analysis for Scheduling Problems using the Inverse Method*. TIME’12, 2012. - [HRSV02]
- T.S. Hune, J.M.T. Romijn, M.I.A. Stoelinga, and F.W. Vaandrager.
*Linear parametric model checking of timed automata*. Journal of Logic and Algebraic Programming, 2002. - [KNS02]
- M. Kwiatkowska, G. Norman, and J. Sproston.
*Probabilistic model checking of the IEEE 802.11 wireless local area network protocol*. In Proc. PAPM/PROBMIV’02, volume 2399 of LNCS, pages 169–187. Springer, 2002. - [KNSW07]
- M. Kwiatkowska, G. Norman, J. Sproston, and F. Wang.
*Symbolic model checking for probabilistic timed automata*. Information and Computation, 205(7):1027–1077, 2007. - [LPPRC10]
- Thi Thieu Hoa Le, Luigi Palopoli, Roberto Passerone, Yusi Ramadian, Alessandro Cimatti.
*Parametric Analysis of Distributed Firm Real-Time Systems: A Case Study*. In ETFA’2010: 1-8. - [Tamura07]
- Naoyuki Tamura. CSP2SAT: JSS benchmark results. 2007.