DARTS.9.1.4.pdf
- Filesize: 0.58 MB
- 6 pages
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
Document Identifiers
Author Details
Acknowledgements
This work was partially supported by MCIN/ AEI /10.13039/501100011033/ FEDER "Una manera de hacer Europa" under grant PID2021-124502OB-C42 (PRESECREL) and by the AIDOaRt project, an ECSEL Joint Under-taking (JU) under grant agreement No. 101007350.
Cite As Get BibTex
Sebastian Altmeyer, Étienne André, Silvano Dal Zilio, Loïc Fejoz, Michael González Harbour, Susanne Graf, J. Javier Gutiérrez, Rafik Henia, Didier Le Botlan, Giuseppe Lipari, Julio Medina, Nicolas Navet, Sophie Quinton, Juan M. Rivas, and Youcheng Sun. From FMTV to WATERS: Lessons Learned from the First Verification Challenge at ECRTS (Artifact). In Special Issue of the 35th Euromicro Conference on Real-Time Systems (ECRTS 2023). Dagstuhl Artifacts Series (DARTS), Volume 9, Issue 1, pp. 4:1-4:6, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
https://doi.org/10.4230/DARTS.9.1.4
Artifact
DARTS-9-1-4-artifact-8a474ddcc9c80e4ffdbbd8f8b1742c1d.zip
(Filesize: 58.35 MB)
MD5 Sum:
8a474ddcc9c80e4ffdbbd8f8b1742c1d
(Get MD5 Sum)
Abstract
We propose here solutions to the FMTV 2015 challenge of a distributed video processing system using four different formalisms, as well as the description of the challenge itself. This artifact contains several solutions to various subchallenges, and instructions and scripts to reproduce these results smoothly.
Subject Classification
ACM Subject Classification
- Computer systems organization → Real-time systems
- Computer systems organization → Embedded systems
- General and reference → Verification
- Software and its engineering → Software verification and validation
Keywords
- Verification challenge
- industrial use case
- end-to-end latency
- real-time systems
- response time analysis
Metrics
- Access Statistics
-
Total Accesses (updated on a weekly basis)
0PDF Downloads
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.