IMITATOR

IMITATOR

Merging Case Studies

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

IMITATOR

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

It can be downloaded from the download page.

Case studies

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 logstatestraces 9 9 0.056 s Yeslogstatestrace set 82 108 =
Flip-Flop [CC07] flipflop.pi0 5 12 11 10 0.06 s Yes logstatestraces 9 9 0.057 s Yeslogstatestrace set 82 95 =
Latch [Andre10] latchValmem.pi0 8 13 18 17 0.083 s ? logstatestraces 12 12 0.069 s ?logstatestrace set 67 83 =
SPSMALL memory [AS13] spsmall.pi0 10 26 31 30 0.618 s Yes logstatestraces 31 30 0.613 s Yeslogstatestrace set 100 99 =
SIMOP [AS13] simop.pi0 8 7 - - Out of memory - - 172 262 2.52 s ?logstatestrace set 0 0 -
BRP [DKRT97] brp.pi0 7 6 429 474 3.5 s Yes logstatestraces 426 473 4.3 s Yeslogstatestrace set 99 123 =
CSMA/CD bc2 [KNSW07] csmacdPrism.pi0 3 3 301 462 0.514 s Yes logstatestraces 300 461 0.574 s Yeslogstatestrace set 100 112 =
CSMA/CD bc6 [KNSW07] csmacdPrism6.pi0 3 3 13365 14271 18.3 s Yes logstatestraces 13365 14271 25.4 s Yeslogstatestrace set 100 139 =
RCP [HRSV02] RCP.pi0 5 6 327 518 0.748 s Yes logstatestraces 115 186 0.684 s Yeslogstatestrace set 35 91 =
WLAN [KNS02] wlan.pi0 2 8 - - Out of memory - - 8430 15152 2137 s Yeslogstatestrace set 0 0 -
ABT [FLMS12] astrium_basic_thermal_fp.pi0 7 7 63 62 0.344 s ? logstatestraces 63 62 0.335 s ?logstatestrace set 100 97 =
AM02 [AM02] am02.pi0 3 4 182 215 0.369 s Yes logstatestraces 53 70 0.112 s Yeslogstatestrace set 29 30
BB04 [BB04] bb.pi0 6 7 806 827 28 s ? logstatestraces 141 145 3.15 s ?logstatestrace set 17 11 =
CTC [???] concurent_tasks_chain.pi0 15 21 1364 1363 88.9 s Yes logstatestraces 215 264 17.6 s Yeslogstatestrace set 16 20 =
LA02 [Tamura07] LA02_2.pi0 3 5 6290 8023 751 s ? logstatestraces 383 533 17.7 s Yeslogstatestrace set 6 2
LPPRC10 [LPPRC10] hppr10_audio.pi0 4 7 78 102 0.39 s ? logstatestraces 31 40 0.251 s ?logstatestrace set 40 64 =
M2.4 [AAM06] maler_2_4.pi0 3 8 1497 1844 8.89 s Yes logstatestraces 119 181 0.374 s Yeslogstatestrace set 8 4

Description of the Case Studies

Hardware circuits

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.

SIMOP

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

Protocols

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.

Scheduling

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.

Algorithms used

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

References

[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.

Contact

Étienne André