Document Open Access Logo

From FMTV to WATERS: Lessons Learned from the First Verification Challenge at ECRTS (Artifact)

Authors 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, Youcheng Sun

PDF

Artifact Description

Thumbnail PDF
PDF
DARTS.9.1.4.pdf
  • Filesize: 0.58 MB
  • 6 pages

Document Identifiers

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)
    0
    PDF Downloads
    0
    Metadata Views

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.

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

Author Details

Sebastian Altmeyer
  • Universität Augsburg, Germany
Étienne André
  • Université Sorbonne Paris Nord, LIPN, CNRS UMR 7030, F-93430 Villetaneuse, France
Silvano Dal Zilio
  • Univ. de Toulouse, INSA, LAAS, F-31400 Toulouse, France
Loïc Fejoz
  • RealTime-at-Work (RTaW), 615, Rue du Jardin Botanique, F-54600 Villers-lès-Nancy, France
Michael González Harbour
  • Universidad de Cantabria, Santander, Spain
Susanne Graf
  • Univ. Grenoble Alpes, CNRS, Grenoble INP, VERIMAG, F-38000 Grenoble, France
J. Javier Gutiérrez
  • Universidad de Cantabria, Santander, Spain
Rafik Henia
  • Thales Research & Technology, F-91767 Palaiseau, France
Didier Le Botlan
  • Univ. de Toulouse, INSA, LAAS, F-31400 Toulouse, France
Giuseppe Lipari
  • Univ. Lille, CNRS, Inria, Centrale Lille, UMR 9189 CRIStAL, F-59000 Lille, France
Julio Medina
  • Universidad de Cantabria, Santander, Spain
Nicolas Navet
  • University of Luxembourg, Luxembourg
Sophie Quinton
  • Univ. Grenoble Alpes, Inria, CNRS, Grenoble INP, LIG, F-38000 Grenoble, France
Juan M. Rivas
  • Universidad de Cantabria, Santander, Spain
Youcheng Sun
  • The University of Manchester, UK

Funding

  • André, Étienne: Partially supported by the ANR-NRF French-Singaporean research program ProMiS (ANR-19-CE25-0015 / 2019 ANR NRF 0092) and ANR BisoUS (ANR-22-CE48-0012).

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.

Artifact

  MD5 Sum: 8a474ddcc9c80e4ffdbbd8f8b1742c1d (Get MD5 Sum)

Related Article

  • 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", in 35th Euromicro Conference on Real-Time Systems (ECRTS 2023), LIPIcs, Vol. 262, pp. 19:1-19:18, 2023. https://doi.org/10.4230/LIPIcs.ECRTS.2023.19

References

  1. 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.
  2. É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.
  3. 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. Google Scholar
  4. 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.
  5. 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.
  6. 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.
  7. 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.
  8. MAST. MAST home Page. URL: https://mast.unican.es.
  9. MAST. MAST models used to get the associated results. URL: http://mast.unican.es/waters15challenge/mastmodels.zip.
  10. 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.
  11. 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.
  12. 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.
  13. 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.
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact