Titre :

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

Auteur(s) :

Altmeyer, Sebastian [Auteur]
Universität Augsburg [Deutschland] = University of Augsburg [Germany] = Université d'Augsburg [Allemagne] [UNIA]
André, Étienne [Auteur]
Laboratoire d'Informatique de Paris-Nord [LIPN]
Dal Zilio, Silvano [Auteur]
Équipe Verification de Systèmes Temporisés Critiques [LAAS-VERTICS]
Fejoz, Loïc [Auteur]
Realtime-at-Work [RTaW]
Harbour, Michael González [Auteur]
Universidad de Cantabria [Santander] = University of Cantabria [Spain] = Université de Cantabrie [Espagne] [UC / UniCan]
Graf, Susanne [Auteur]
VERIMAG [VERIMAG - IMAG]
Gutiérrez, J. Javier [Auteur]
Universidad de Cantabria [Santander] = University of Cantabria [Spain] = Université de Cantabrie [Espagne] [UC / UniCan]
Henia, Rafik [Auteur]
THALES [France]
Le Botlan, Didier [Auteur]
Équipe Verification de Systèmes Temporisés Critiques [LAAS-VERTICS]
Lipari, Giuseppe [Auteur]
Analyse symbolique et conception orientée composants pour des systèmes embarqués temps-réel modulaires [SYCOMORES]
Centre de Recherche en Informatique, Signal et Automatique de Lille - UMR 9189 [CRIStAL]
Medina, Julio [Auteur]
Universidad de Cantabria [Santander] = University of Cantabria [Spain] = Université de Cantabrie [Espagne] [UC / UniCan]
Navet, Nicolas [Auteur]
Université du Luxembourg = University of Luxembourg = Universität Luxemburg [uni.lu]
Quinton, Sophie [Auteur]
Pôle d'ingénierie multidisciplinaire du LIG [PIMLIG ]
Rivas, Juan [Auteur]
Universidad de Cantabria [Santander] = University of Cantabria [Spain] = Université de Cantabrie [Espagne] [UC / UniCan]
Sun, Youcheng [Auteur]
University of Manchester [Manchester]

Éditeur(s) ou directeur(s) scientifique(s) :

Alessandro V. Papadopoulos

Titre de la manifestation scientifique :

35th Euromicro Conference on Real-Time Systems (ECRTS 2023)

Ville :

Vienne

Pays :

Autriche

Date de début de la manifestation scientifique :

2023-07-11

Titre de l’ouvrage :

Leibniz International Proceedings in Informatics (LIPIcs)

Titre de la revue :

35th Euromicro Conference on Real-Time Systems (ECRTS 2023)

Éditeur :

Schloss Dagstuhl – Leibniz-Zentrum für Informatik

Date de publication :

2023

Mot(s)-clé(s) en anglais :

Verification challenge
industrial use case
end-to-end latency

Discipline(s) HAL :

Informatique [cs]/Génie logiciel [cs.SE]
Informatique [cs]/Systèmes et contrôle [cs.SY]

Résumé en anglais : [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 ...
Lire la suite >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.Lire moins >

Langue :

Anglais

Comité de lecture :

Oui

Audience :

Internationale

Vulgarisation :

Non

Projet ANR :

Mitigation formelle d'attaques via canaux auxiliaires par vérification paramétrée
Better Synthesis for Underspecified Quantitative Systems

Collections :

• Centre de Recherche en Informatique, Signal et Automatique de Lille (CRIStAL) - UMR 9189

Source :

Harvested from HAL