Publications related to IMITATOR

Book on the inverse method

É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

É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]

Latest poster on IMITATOR

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

Publications describing algorithms in IMITATOR

É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]
É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]
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)
É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]
É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]
É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]
É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]
É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]
É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]
É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]
É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]
É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]
É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

É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, January 2019. To appear. (English)
É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]
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
É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]
Lăcrămioara Aştefănoaei, Saddek Bensalem, Marius Bozga, Chih-Hong Cheng, Harald Ruess: Compositional Parameter Synthesis. FM 2016: 60-68
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)]
Chih-Hong Cheng, Lăcrămioara Aştefănoaei, Souha Ben-Rayana and Saddek Bensalem. Timed Orchestration for Component-based Systems. arXiv:1504.05513v1.
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.
É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)]
Léa Fanchon and Florent Jacquemard Formal Timing Analysis Of Mixed Music Scores. International Computer Music Conference (ICMC) 2013.
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]
É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]
L. Fribourg, D. Lesens, P. Moro and R. SoulatRobustness Analysis for Scheduling Problems using the Inverse Method. In TIME’12, pages 73-80. IEEE Computer Society Press, 2012. ( PDF | BibTeX + Abstract )
Romain Soulat. Scheduling with IMITATOR: Some Case Studies. Research Report, Laboratoire Spécification et Vérification, March 2012.
É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.

Library of benchmarks

Étienne André. A benchmarks library for parametric timed model checking. In Cyrille Artho and Peter Csaba Ölveczky (eds.), FTSCS’18, Springer CCIS, November 2018. To appear. (English)

Former tool paper

É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]