Document
From FMTV to WATERS: Lessons Learned from the First Verification Challenge at ECRTS (Artifact)
Authors
Étienne André 
,
Silvano Dal Zilio ,
Susanne Graf ,
Didier Le Botlan ,
Giuseppe Lipari ,
Youcheng Sun
-
Part of:
Issue:
Special Issue of the 35th Euromicro Conference on Real-Time Systems (ECRTS 2023)
Volume: DARTS, Volume 9 (ECOOP 2023)
Conference: Euromicro Conference on Real-Time Systems (ECRTS)
Journal: Dagstuhl Artifacts Series (DARTS) - License:
Creative Commons Attribution 4.0 International license
- Publication Date: 2023-07-03
Artifact Description
PDF
DARTS.9.1.4.pdf
- Filesize: 0.58 MB
- 6 pages
Author Details
References
- Rajeev Alur, Thomas A. Henzinger, and Moshe Y. Vardi. Parametric real-time reasoning. In S. Rao Kosaraju, David S. Johnson, and Alok Aggarwal, editors, STOC, pages 592-601, New York, NY, USA, 1993. ACM. URL: https://doi.org/10.1145/167088.167242.
- Étienne André. IMITATOR 3: Synthesis of timing parameters beyond decidability. In Rustan Leino and Alexandra Silva, editors, CAV, volume 12759 of Lecture Notes in Computer Science, pages 1-14. Springer, 2021. URL: https://doi.org/10.1007/978-3-030-81685-8_26.
-
Bernard Berthomieu, Jean-Paul Bodeveix, Patrick Farail, Mamoun Filali, Hubert Garavel, Pierre Gauffilet, Frédéric Lang, and François Vernadat. Fiacre: an intermediate language for model verification in the TOPCASED environment. In Embedded Real Time Software, 2008.
- Bernard Berthomieu, Pierre-Olivier Ribet, and François Vernadat. The tool TINA - construction of abstract state spaces for Petri nets and time Petri nets. International Journal of Production Research, 42(14):2741-2756, 2004. URL: https://doi.org/10.1080/00207540412331312688.
- Silvano Dal Zilio, Bernard Berthomieu, and Didier Le Botlan. Latency Analysis of an Aerial Video Tracking System Using Fiacre and Tina. Technical Report 15355, LAAS-CNRS, 2015. This work was presented at the FMTV verification challenge of WATERS 2015, the 6th International Workshop on Analysis Tools and Methodologies for Embedded and Real-time Systems. URL: https://hal.science/hal-01202741.
- Michael González Harbour, J. Javier Gutiérrez García, José Carlos Palencia Gutiérrez, and J. M. Drake Moyano. MAST: Modeling and analysis suite for real time applications. In ECRTS, pages 125-134. IEEE Computer Society, 2001. URL: https://doi.org/10.1109/EMRTS.2001.934015.
- Kim Guldstrand Larsen, Paul Pettersson, and Wang Yi. UPPAAL in a nutshell. International Journal on Software Tools for Technology Transfer, 1(1-2):134-152, 1997. URL: https://doi.org/10.1007/s100090050010.
- MAST. MAST home Page. URL: https://mast.unican.es.
- MAST. MAST models used to get the associated results. URL: http://mast.unican.es/waters15challenge/mastmodels.zip.
- MAST. Version of the MAST tool used to get the associated results. URL: http://mast.unican.es/mast-bin-win-1-5-0-1.zip.
- Julio L. Medina, Juan M. Rivas, J. Javier Gutiérrez, and Michael González Harbour. Solving the 2015 FMTV challenge using response time analysis with MAST. Solutions to the FMTV Challenge, Informal proceedings of the 6th International Workshop on Analysis Tools and Methodologies for Embedded and Real-time Systems (WATERS 2015), July 2015. URL: https://www.ecrts.org/forum/download/FMTV15_Solution_MAST.pdf.
- Lijun Shan and Susanne Graf. Timing verification of an aerial video tracking system using UPPAAL. Solutions to the FMTV Challenge, Informal proceedings of the 6th International Workshop on Analysis Tools and Methodologies for Embedded and Real-time Systems (WATERS 2015), July 2015. URL: https://www.ecrts.org/forum/download/FMTV15_Solution_UPPAAL.pdf.
- Youcheng Sun, Étienne André, and Giuseppe Lipari. Verification of two real-time systems using parametric timed automata. Solutions to the FMTV Challenge, Informal proceedings of the 6th International Workshop on Analysis Tools and Methodologies for Embedded and Real-time Systems (WATERS 2015), July 2015. URL: https://www.ecrts.org/forum/download/FMTV15_Solution_Parametric_Timed_Automata.pdf.