IMITATOR

Publications related to IMITATOR

Book on the inverse method

[AS13]
Étienne André and Romain Soulat. The Inverse Method. ISTE Ltd and John Wiley & Sons Inc. ISBN: 9781848214477. January 2013. (English) [PDF | BibTeX]

Latest tool paper on IMITATOR

[Andre21]
Étienne André. IMITATOR 3: Synthesis of timing parameters beyond decidability. In Rustan Leino and Alexandra Silva (eds.), CAV’21, Springer LNCS 12759, pages 1-14, July 2021. DOI: 10.1007/978-3-030-81685-8_26 Creative Commons Attribution 3.0 Unported (CC BY 3.0) (English) [data | Slides]🌐

Latest poster on IMITATOR

[IMITATOR18]
Étienne André. IMITATOR: parametric verification of real-time systems. WINTERFESTA’18, December 2018. (English) [PDF (author version)]

Publications describing algorithms in IMITATOR

[AA22]
Johan Arcile and Étienne André. Zone extrapolations in parametric timed automata. In Klaus Havelund, Jyotirmoy V. Deshmukh and Ivan Perez (eds.), NFM’22, Springer LNCS 13260, pages 451-469, May 2022. DOI: 10.1007/978-3-031-06773-0_24 (English) [PDF (author version) | data]🌐
[AAPP21]
Étienne André, Jaime Arias, Laure Petrucci and Jaco van de Pol. Iterative bounded synthesis for efficient cycle detection in parametric timed automata. In Jan Friso Groote and Kim G. Larsen (eds.), TACAS’21, March 2021. To appear. Creative Commons Attribution 3.0 Unported (CC BY 3.0) (English) [data]
[ABPP19]
Étienne André, Vincent Bloemen, Laure Petrucci and Jaco van de Pol. Minimal-Time Synthesis for Parametric Timed Automata. In Tomáš Vojnar and Lijun Zhang (eds.), TACAS’19, Springer LNCS 11428, pages 211–228, April 2019. Acceptance rate: 30%. DOI: 10.1007/978-3-030-17465-1_12 Creative Commons Attribution 3.0 Unported (CC BY 3.0) (English) [PDF | PDF (author version) | BibTeX | data]🌐
[ALR18ACSD]
Étienne André, Didier Lime and Mathias Ramparison. Timed automata with parametric resets. In Thomas Chatain and Radu Grosu (eds.), ACSD’18, IEEE, pages 21–29, June 2018. (English) [PDF (author version) | BibTeX | Slides]
[NPP18]
Nguyễn Hoàng Gia, Laure Petrucci, Jaco van de Pol: Layered and Collecting NDFS with Subsumption for Parametric Timed Automata. ICECCS 2018: 1-9🌐
[ALin17]
Étienne André and Lin Shang-Wei (林尚威). Learning-based compositional parameter synthesis for event-recording automata. In Ahmed Bouajjani and Alexandra Silva (eds.), FORTE’17, Springer LNCS 10321, pages 17–32, June 2017. (English) [PDF (author version) | BibTeX | Slides]🌐
[LSGA17]
Li Jiaying, Sun Jun, Gao Bo (高博) and Étienne André. Classification based Parameter Synthesis for Parametric Timed Automata. In Zhenhua Duan and Luke Ong (eds.), ICFEM’17, Springer LNCS 10610, pages 243–261, November 2017. (English)🌐
[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]
[ANPS17]
Étienne André, Nguyễn Hoàng Gia, Laure Petrucci and Sun Jun. Parametric model checking timed automata under non-Zenoness assumption. In Clark Barrett, Misty Davies and Temesghen Kahsai (eds.), NFM’17, Springer LNCS 10227, pages 35–51, May 2017. (English) [BibTeX | Slides]
[ALNS15]
Étienne André, Giuseppe Lipari, Nguyễn Hoàng Gia and Sun Youcheng. Reachability Preservation Based Parameter Synthesis for Timed Automata. In Klaus Havelund, Gerard Holzmann, Rajeev Joshi (eds.), NFM’15, LNCS 9058, Springer, pages 50–65, April 2015. (English) [PDF | PDF (author version) | BibTeX | Slides]
[ACE14]
Étienne André, Camille Coti and Sami Evangelista. Distributed Behavioral Cartography of Timed Automata. In Jack Dongarra, Yutaka Ishikawa, and Atsushi Hori (eds.), EUROMPI/ASIA’14, ACM, September 2014. (English) [PDF (author version) | BibTeX | Slides]
[AFS13atva]
Étienne André, Laurent Fribourg and Romain Soulat. Merge and Conquer: State Merging in Parametric Timed Automata. In Hung Dang-Van and Mizuhito Ogawa (eds.), ATVA’13, LNCS 8172, Springer, pages 381–396, October 2013. [PDF (author version) | PDF (long author version) | BibTeX | Slides]
[Andre13FSFMA]
Étienne André. Dynamic Clock Elimination in Parametric Timed Automata. In Christine Choppy and Jun Sun (eds.), FSFMA’13, OASIcs (volume 31), Schloss Dagstuhl – Leibniz-Zentrum für Informatik, Dagstuhl Publishing, pages 18–31, July 2013. Creative Commons Attribution 3.0 Unported (CC BY 3.0) (English) [PDF | BibTeX | Slides]
[Andre13ICECCS]
Étienne André. Observer Patterns for Real-Time Systems. In Yang Liu and Andrew Martin (eds.), ICECCS’13, pages 125–134, July 2013. (English) [PDF (author version) | BibTeX | Slides]
[AS11]
Étienne André and Romain Soulat. Synthesis of Timing Parameters Satisfying Safety Properties. In Giorgio Delzanno and Igor Potapov (eds.), RP’11, LNCS 6945, Springer, pages 31–44, 2011. (English) [PDF (author version) | PDF (long author version) | BibTeX]
[AF10]
Étienne André and Laurent Fribourg. Behavioral Cartography of Timed Automata. In Antonín Kučera and Igor Potapov (eds.), RP’10, LNCS 6227, Springer, pages 76–90, September 2010. (English) [PDF (published version) | PDF (author version) | BibTeX | Slides]
[ACEF09]
Étienne André, Thomas Chatain, Emmanuelle Encrenaz and Laurent Fribourg. An Inverse Method for Parametric Timed Automata. International Journal of Foundations of Computer Science 20(5), pages 819–836, 2009. (English) [PDF (published version) | PDF (author version) | BibTeX]

Publications describing verifications using IMITATOR

[ACFJL21]
Étienne André, Emmanuel Coquard, Laurent Fribourg, Jawher Jerray and David Lesens. Parametric schedulability analysis of a launcher flight control system under reactivity constraints. Fundamenta Informatica. 2021. To appear.
[ABPPSS20]
Jaime Arias, Carlos E. Budde, Wojciech Penczek, Laure Petrucci, Teofil Sidoruk, Mariëlle Stoelinga: Hackers vs. Security: Attack-Defence Trees as Asynchronous Multi-agent Systems. ICFEM 2020: 3-19🌐
[AK20]
Étienne André and Aleksander Kryukov. Parametric non-interference in timed automata. In Yi Li and Alan Liew (eds.), ICECCS’20, October 2020. To appear. (English) [PDF (author version) | data]🌐
[LGSBL19]
Lars Luthmann, Timo Gerecht, Andreas Stephan, Johannes Bürdek, Malte Lochau: Minimum/maximum delay testing of product lines with unbounded parametric real-time constraints. Journal of Systems and Software 149: 535-553 (2019)🌐
[AS19]
Étienne André and Sun Jun. Parametric timed model checking for guaranteeing timed opacity. In Yu-Fang Chen, Chih-Hong Cheng and Javier Esparza (eds.), ATVA’19, Springer LNCS 11781, pages 115–130, October 2019. DOI: 10.1007/978-3-030-31784-3_7 (English) [PDF (author version) | BibTeX | data | Slides]🌐
[ALRS19]
Étienne André, Didier Lime, Mathias Ramparison and Mariëlle Stoelinga. Parametric analyses of attack-fault trees. In Jörg Keller and Wojciech Penczek (eds.), ACSD’19, IEEE, pages 33–42, June 2019. DOI: 10.1109/ACSD.2019.00008 (English) [PDF (author version) | BibTeX | data]🌐
[AAGR19]
Étienne André, Paolo Arcaini, Angelo Gargantini and Marco Radavelli. Repairing timed automata clock guards through abstraction and testing. In Dirk Beyer and Chantal Keller (eds.), TAP’19, Springer LNCS 11823, pages 129–146, October 2019. DOI: 10.1007/978-3-030-31157-5_9 (English) [PDF (author version) | BibTeX | data]🌐
[ACFJL19]
Étienne André, Emmanuel Coquard, Laurent Fribourg, Jawher Jerray and David Lesens. Parametric schedulability analysis of a launcher flight control system under reactivity constraints. In Jörg Keller and Wojciech Penczek (eds.), ACSD’19, IEEE, pages 13–22, June 2019. DOI: 10.1109/ACSD.2019.00006 (English) [PDF (author version) | BibTeX | data]🌐
[AFMS19]
Étienne André, Laurent Fribourg, Jean-Marc Mota and Romain Soulat. Verification of an industrial asynchronous leader election algorithm using abstractions and parametric model checking. In Constantin Enea and Ruzica Piskac (eds.), VMCAI’19, Springer LNCS 11388, pages 409–424, January 2019. Acceptance rate: 44%. DOI: 10.1007/978-3-030-11245-5_19 (English) [PDF | PDF (author version) | BibTeX | Slides]🌐
[WA19]
Masaki Waga (和賀 正樹) and Étienne André. Online Parametric Timed Pattern Matching with Automata-Based Skipping. In Julia Badger and Kristin Yvonne Rozier (eds.), NFM’19, Springer LNCS 11460, pages 371–389, May 2019. DOI: 10.1007/978-3-030-20652-9_26 (English) [PDF | PDF (author version) | BibTeX | data]🌐
[AHW18]
Étienne André, Ichiro Hasuo and Masaki Waga (和賀 正樹). Offline timed pattern matching under uncertainty. In Anthony Widjaja Lin and Jun Sun (eds.), ICECCS’18, IEEE CPS, pages 10–10, December 2018. (English) [BibTeX | Slides]
[LSB17]
Lars Luthmann, Andreas Stephan, Johannes Bürdek, Malte Lochau: Modeling and Testing Product Lines with Unbounded Parametric Real-Time Constraints. SPLC (A) 2017: 104-113🌐
[Andre17FMICS]
Étienne André. A unified formalism for monoprocessor schedulability analysis under uncertainty. In Laure Petrucci, Cristina Seceleanu and Ana Cavalcanti (eds.), FMICS-AVoCS’17, Springer LNCS 10471, pages 100–115, September 2017. (English) [PDF (author version) | BibTeX | Slides]
[ABBCR16]
Lăcrămioara Aştefănoaei, Saddek Bensalem, Marius Bozga, Chih-Hong Cheng, Harald Ruess: Compositional Parameter Synthesis. FM 2016: 60-68
[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)]
[CABB15]
Chih-Hong Cheng, Lăcrămioara Aştefănoaei, Souha Ben-Rayana and Saddek Bensalem. Timed Orchestration for Component-based Systems. arXiv:1504.05513v1.
[LSAF14]
Giuseppe Lipari, Sun Youcheng, Étienne André and Laurent Fribourg. Toward Parametric Timed Interfaces for Real-Time Components. In Étienne André and Goran Frehse (eds.), SynCoP’14, EPTCS, April 2014.
[AKP14]
Étienne André, Fabrice Kordon and Laure Petrucci. Teaching Formal Methods: Experience at UPMC and UP13 with CosyVerif. In Bahar Karaoglan (eds.), EAEEIE’14, IEEE, pages 31–34, May 2014. (English) [PDF (author version)]
[FJ13]
Léa Fanchon and Florent Jacquemard. Formal Timing Analysis Of Mixed Music Scores. International Computer Music Conference (ICMC) 2013.
[SSLAF13]
Sun Youcheng, Romain Soulat, Giuseppe Lipari, Étienne André and Laurent Fribourg. Parametric Schedulability Analysis of Fixed Priority Real-Time Distributed Systems. In Cyrille Artho and Peter Ölveczky (eds.), FTSCS’13, Volume 419 of Communications in Computer and Information Science, Springer, pages 212–228, October 2013. (English) [PDF (author version) | Slides]
[AFS13FMSD]
Étienne André, Laurent Fribourg and Jeremy Sproston. An Extension of the Inverse Method to Probabilistic Timed Automata. Formal Methods in System Design 42(2), pages 119–145, April 2013. (English) [PDF (published version) | PDF (author version) | BibTeX]
[FLMS12]
L. Fribourg, D. Lesens, P. Moro and R. Soulat.  Robustness Analysis for Scheduling Problems using the Inverse Method. In TIME’12, pages 73-80. IEEE Computer Society Press, 2012. ( PDF | BibTeX + Abstract )
[Soulat12]
Romain Soulat. Scheduling with IMITATOR: Some Case Studies. Research Report, Laboratoire Spécification et Vérification, March 2012.
[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.

Translation from real-time systems to the IMITATOR input format

[AJM19]
Étienne André, Jawher Jerray and Sahar Mhiri. Time4sys2imi: A tool to formalize real-time system models under uncertainty. In Robert M. Hierons and Mohamed Mosbah (eds.), ICTAC’19, Springer LNCS, pages 113–123, November 2019. Acceptance rate: 14%. DOI: 10.1007/978-3-030-32505-3_7 (English) [PDF (author version) | BibTeX | data]🌐
[Andre19]
Étienne André. Formalizing Time4sys using parametric timed automata. In Dominique Méry and Shengchao Qin (eds.), TASE’19, IEEE, pages 176–183, July 2019. DOI: 10.1109/TASE.2019.00031 (English) [PDF (author version) | BibTeX | Slides]🌐

Library of benchmarks

[Andre18]
Étienne André. A benchmarks library for parametric timed model checking. In Cyrille Artho and Peter Csaba Ölveczky (eds.), FTSCS’18, Springer CCIS 1008, pages 75–83, November 2018. Acceptance rate: 45%. DOI: 10.1007/978-3-030-12988-0_5 (English) [PDF (author version) | BibTeX | data | Slides]🌐

Old tool papers

[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]🌐
[Andre10infinity]
Étienne André. IMITATOR II: A Tool for Solving the Good Parameters Problem in Timed Automata. In Yu-Fang Chen and Ahmed Rezine (eds.), INFINITY’10, Electronic Proceedings in Theoretical Computer Science 39, pages 91–99, 2010. Creative Commons Attribution 3.0 Unported (CC BY 3.0) (English) [PDF (published version) | BibTeX | Slides]