Verification challenge; industrial use case; end-to-end latency
Résumé :
[en] We present here the main features and lessons learned from the first edition of what has now become the ECRTS industrial challenge, together with the final description of the challenge and a comparative overview of the proposed solutions. This verification challenge, proposed by Thales, was first discussed in 2014 as part of a dedicated workshop (FMTV, a satellite event of the FM 2014 conference), and solutions were discussed for the first time at the WATERS 2015 workshop. The use case for the verification challenge is an aerial video tracking system. A specificity of this system lies in the fact that periods are constant but known with a limited precision only. The first part of the challenge focuses on the video frame processing system. It consists in computing maximum values of the end-to-end latency of the frames sent by the camera to the display, for two different buffer sizes, and then the minimum duration between two consecutive frame losses. The second challenge is about computing end-to-end latencies on the tracking and camera control for two different values of jitter. Solutions based on five different tools - Fiacre/Tina, CPAL (simulation and analysis), IMITATOR, UPPAAL and MAST - were submitted for discussion at WATERS 2015. While none of these solutions provided a full answer to the challenge, a combination of several of them did allow to draw some conclusions.
Disciplines :
Sciences informatiques
Auteur, co-auteur :
Altmeyer, Sebastian; University of Augsburg, Germany
André, Etienne; Université Sorbonne Paris Nord, France
Dal Zilio, Silvano; University of Toulouse, France
Fejoz, Loïc; RealTime-at-Work
Harbour, Michael González; University of Cantabria, Spain
Graf, Susanne; University of Grenoble Alpes, France
Gutiérrez, J. Javier; University of Cantabria, Spain
Henia, Rafik; Thales Research & Technology
Le Botlan, Didier; University of Toulouse, France
Lipari, Giuseppe; University of Lille, France
Medina, Julio; University of Cantabria, Spain
NAVET, Nicolas ; University of Luxembourg > Faculty of Science, Technology and Medicine (FSTM) > Department of Computer Science (DCS)
Quinton, Sophie; University of Grenoble Alpes, France
Sebastian Altmeyer, Loïc Fejoz, and Nicolas Navet. Using CPAL to model and validate the timing behaviour of embedded systems. 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://nicolas.navet.eu/publi/challenge.pdf.
Rajeev Alur and David L. Dill. A theory of timed automata. Theoretical Computer Science, 126(2):183–235, April 1994. doi:10.1016/0304-3975(94)90010-8.
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. doi:10.1145/167088.167242.
Andoni Amurrio, Ekain Azketa, J. Javier Gutiérrez, Mario Aldea Rivas, and Michael González Harbour. Response-time analysis of multipath flows in hierarchically-scheduled time-partitioned distributed real-time systems. IEEE Access, 8:196700–196711, 2020. doi: 10.1007/s10009-017-0467-0.
É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. doi:10.1007/978-3-030-81685-8_26.
Étienne André, Emmanuel Coquard, Laurent Fribourg, Jawher Jerray, and David Lesens. Parametric schedulability analysis of a launcher flight control system under reactivity constraints. Fundamenta Informaticae, 182(1):31–67, September 2021. doi:10.3233/FI-2021-2065.
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 (ERTS), 2008.
Bernard Berthomieu, Silvano Dal Zilio, and Didier Le Botlan. Latency analysis of an aerial video tracking system using Fiacre and Tina. 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_Fiacre_Tina.pdf.
Bernard Berthomieu and François Vernadat. Time Petri nets analysis with TINA. In QEST, pages 123–124. IEEE Computer Society, 2006. doi:10.1109/QEST.2006.56.
CPAL: A Cyber-Physical Action Language. URL: https://www.designcps.com/model-based-design-with-cpal/.
Formal Methods for Timing Verification (FMTV) Workshop, a satellite event of FM’14, the 19th International Symposium on Formal Methods. URL: https://www.comp.nus.edu.sg/~pat/FM2014/.
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. doi:10.1109/EMRTS.2001.934015.
Rafik Henia. Consolidated version of the WATERS industrial challenge by Thales including a corresponding model in Papyrus. URL: https://www.ecrts.org/forum/viewtopic26ef.html?f=34&t=86&sid=d74079af129d5480a5ac4fd1778eecc1.
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. doi:10.1007/ s100090050010.
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.
Philip Meir Merlin. A study of the recoverability of computing systems. PhD thesis, University of California, Irvine, CA, USA, 1974.
Baptiste Parquier, Laurent Rioux, Rafik Henia, Romain Soulat, Olivier H. Roux, Didier Lime, and Étienne André. Applying parametric model-checking techniques for reusing real-time critical systems. In Cyrille Artho and Peter Csaba Ölveczky, editors, FTSCS, volume 694 of Communications in Computer and Information Science, pages 129–144. Springer, November 2016. doi:10.1007/978-3-319-53946-1_8.
Juan Maria Rivas, J. Javier Gutiérrez, Mario Aldea Rivas, César Cuevas, Michael González Harbour, José María Drake, Julio L. Medina, Laurent Rioux, Rafik Henia, and Nicolas Sordon. An experience integrating response-time analysis and optimization with an MDE strategy. In Paolo Milazzo, Dániel Varró, and Manuel Wimmer, editors, MELO @ STAF, volume 9946 of Lecture Notes in Computer Science, pages 303–316. Springer, 2016. doi: 10.1007/978-3-319-50230-4_23.
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. https://lipn.univ-paris13.fr/ andre/documents/verification-of-two-real-time-systems-using-parametric-timed-automata.pdf.
Youcheng Sun, Étienne André, and Giuseppe Lipari. Verification of an aerial video system. Solutions to the consolidated 2015 industrial Challenge, Informal proceedings of the 8th International Workshop on Analysis Tools and Methodologies for Embedded and Real-time Systems (WATERS 2017), July 2017. URL: https://www.ecrts.org/forum/download/FMTV17_submitted.pdf.
Website of the WATERS’15 workshop. URL: http://waters2015.inria.fr/.
