Case Studies Related to Efficient Parameter Synthesis Using Optimized State Exploration Strategies
This page is dedicated to the case studies related to the manuscript
Efficient Parameter Synthesis Using Optimized State Exploration Strategies
by Étienne André, Hoang Gia Nguyen, and Laure Petrucci,
published in the proceedings of the ICECCS’17 [ANP17].
IMITATOR
The version of IMITATOR used to run the experiments is IMITATOR 2.9.2-working (branch explorder (merged into master branch since), build 2363, GitHub hash 5c40e39).
A (rebuilt) binary from this version of the code is available here (static binary for Linux 64 bits).
Case studies
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).
Standard version of EF
EF with states merging
EFcounterexample
EFcounterexample with state merging
Description of the Case Studies
CSMA/CD
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.
Fischer
This is a model of Fischer’s mutual exclusion protocol proposed in [AHV93].
RCP (Root Contention Protocol)
This is a model of IEEE 1394 Root Contention Protocol.
WFAS (wireless fire alarm system)
This is a model of a wireless fire alarm system studied in [BBLS15].
AndOr circuit
This small asynchronous circuit consists in an AND gate connected to an OR gate in a cyclic manner; its behavior is studied in [CC05].
Flip-flop circuit
This asynchronous circuit consists of several gates connected to each other in a cyclic manner; its behavior is studied in [CC04].
Sched5
This is the model of the schedulability of 5 fixed-priority tasks in a single processor.
SIMOP
This is a model of a networked automation system studied in [ACDFR09].
Train-gate-controller
This is a model of a train-gate-controller from here.
coffee
This is a model of a simple coffee machine used as a teaching example.
CUBPTA1
This is a toy case study to illustrate and test CUB-PTAs.
JLR15
This is a case study studied in [JLR15].
Algorithms used
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
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.
- [AFKS12]
- Étienne André, Laurent Fribourg, Ulrich Kühne and Romain Soulat. IMITATOR 2.5: A Tool for Analyzing Robustness in Scheduling Problems. In Dimitra Giannakopoulou and Dominique Méry (eds.), FM’12, LNCS 7436, Springer, pages 33–36, August 2012. (English) [PDF | PDF (author version) | BibTeX]🌐
- [AHV93]
- Rajeev Alur, Thomas A. Henzinger, Moshe Y. Vardi: Parametric real-time reasoning. STOC 1993: 592-601.
- [ANP17]
- Étienne André, Nguyễn Hoàng Gia and Laure Petrucci. Efficient parameter synthesis using optimized state exploration strategies. In Zhenjiang Hu and Guangdong Bai, (eds.), ICECCS’17, IEEE CPS, pages 1–10, November 2017. (English) [PDF (author version) | BibTeX | Slides]
- [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.
- [CC07]
- Robert Clarisó, Jordi Cortadella. The Octahedron Abstract Domain. In Science of Computer Programming 64(1), pages 115-139, 2007.
- [CEFX09]
- Rémy Chevallier, Emmanuelle Encrenaz-Tiphène, Laurent Fribourg, and Weiwen Xu. Timed verification of the generic architecture of a memory circuit using parametric timed automata. Formal Methods in System Design, 34(1):59–81, 2009.
- [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).
- [DKRT97]
- Pedro R. D’Argenio, Joost-Pieter Katoen, Theo C. Ruys, Jan Tretmans: The Bounded Retransmission Protocol Must Be on Time! TACAS 1997: 416-431.
- [HT15]
- Frédéric Herbreteau, Thanh-Tung Tran:
Improving Search Order for Reachability Testing in Timed Automata. FORMATS 2015: 124-139🌐
- [JLR13]
- Aleksandra Jovanović, Didier Lime, and Olivier H. Roux. Integer parameter synthesis for timed automata. In TACAS, volume 7795 of Lecture Notes in Computer Science, pages 401–415. Springer, 2013.
- [JLR15]
- Aleksandra Jovanović, Didier Lime, and Olivier H. Roux. Integer parameter synthesis for real-time systems. IEEE Transactions on Software Engeneering 41(5): 445-461 (2015).
- [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.
- [KP12]
- Michał Knapik, Wojciech Penczek:
Bounded Model Checking for Parametric Timed Automata. Trans. Petri Nets and Other Models of Concurrency 5: 141-159 (2012)
- [PS08]
- Wojciech Penczek, Maciej Szreter. SAT-based Unbounded Model Checking of Timed Automata. Fundam. Inform. 85(1-4): 425-440 (2008)
- [SAL15]
- Sun Youcheng, Étienne André and Giuseppe Lipari. Verification of Two Real-Time Systems Using Parametric Timed Automata. In Sophie Quinton and Tullio Vardanega (eds.), WATERS’15, July 2015. (English) [PDF (author version)]
- [TY01]
- Stavros Tripakis, Sergio Yovine:
Analysis of Timed Systems Using Time-Abstracting Bisimulations. Formal Methods in System Design 18(1): 25-68 (2001)🌐
Contact
Étienne André
![[AndOr-pta.jpg]](explorder-case-studies/AndOr-pta.jpg){kind=link}
![[flipflop-pta.jpg]](explorder-case-studies/flipflop-pta.jpg){kind=link}
![[BRP-pta.jpg]](explorder-case-studies/BRP-pta.jpg){kind=link}
![[fmtv1A1-v2-pta.jpg]](explorder-case-studies/fmtv1A1-v2-pta.jpg){kind=link}
![[fmtv1A3-v2-pta.jpg]](explorder-case-studies/fmtv1A3-v2-pta.jpg){kind=link}
![[Sched2.100.0-pta.jpg]](explorder-case-studies/Sched2.100.0-pta.jpg){kind=link}
![[Sched2.100.2-pta.jpg]](explorder-case-studies/Sched2.100.2-pta.jpg){kind=link}
![[Sched2.50.0-pta.jpg]](explorder-case-studies/Sched2.50.0-pta.jpg){kind=link}
![[Sched2.50.2-pta.jpg]](explorder-case-studies/Sched2.50.2-pta.jpg){kind=link}
![[FDDI-pta.jpg]](explorder-case-studies/FDDI-pta.jpg){kind=link}
![[FDDI4-pta.jpg]](explorder-case-studies/FDDI4-pta.jpg){kind=link}
![[fischer-pta.jpg]](explorder-case-studies/fischer-pta.jpg){kind=link}
![[fischer3-pta.jpg]](explorder-case-studies/fischer3-pta.jpg){kind=link}
![[lynch-pta.jpg]](explorder-case-studies/lynch-pta.jpg){kind=link}
![[lynch5-pta.jpg]](explorder-case-studies/lynch5-pta.jpg){kind=link}
![[F3-pta.jpg]](explorder-case-studies/F3-pta.jpg){kind=link}
![[F4-pta.jpg]](explorder-case-studies/F4-pta.jpg){kind=link}
![[Pipeline-KP12-2-3-pta.jpg]](explorder-case-studies/Pipeline-KP12-2-3-pta.jpg){kind=link}
![[Pipeline-KP12-2-5-pta.jpg]](explorder-case-studies/Pipeline-KP12-2-5-pta.jpg){kind=link}
![[Pipeline-KP12-3-3-pta.jpg]](explorder-case-studies/Pipeline-KP12-3-3-pta.jpg){kind=link}
![[RCP-pta.jpg]](explorder-case-studies/RCP-pta.jpg){kind=link}
![[spsmall-pta.jpg]](explorder-case-studies/spsmall-pta.jpg){kind=link}
![[critical-region-pta.jpg]](explorder-case-studies/critical-region-pta.jpg){kind=link}
![[critical-region4-pta.jpg]](explorder-case-studies/critical-region4-pta.jpg){kind=link}
![[blowup-para1001-pta.jpg]](explorder-case-studies/blowup-para1001-pta.jpg){kind=link}
