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

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

Latest poster on IMITATOR

[ALS15]
Étienne André, Giuseppe Lipari and Sun Youcheng. IMITATOR: Formal Verification of Real-Time Systems Under Uncertainty. In Steve Goddard and Harini Ramaprasad (eds.), ECRTS’15 posters, July 2015. Creative Commons Attribution-ShareAlike 3.0 Unported (CC BY-SA 3.0) (English) [PDF]

Publications describing algorithms in IMITATOR

[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 and Temesghen Kahsai (eds.), NFM’17, Springer LNCS, May 2017. To appear.
[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)]
[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

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

Former tool paper

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