Bridging the Gap between Formal Verification and Schedulability Analysis: The Case of Robotics - LAAS - Laboratoire d'Analyse et d'Architecture des Systèmes Accéder directement au contenu
Article Dans Une Revue Journal of Systems Architecture Année : 2020

Bridging the Gap between Formal Verification and Schedulability Analysis: The Case of Robotics

Mohammed Foughali

Résumé

The challenges of deploying robots and autonomous vehicles call for further efforts to bridge the gap between the robotics, the real-time systems and the formal methods communities. Indeed, with robots being more and more involved in costly missions and contact with humans, a rigorous formal verification of their behavior in the presence of various real-time constraints is crucial. In order to increase our trust in its results, such verification should be carried out on models that are the closest possible to reality, and thus take into account hardware and OS specificities such as the number of cores provided by the robotic platform and the scheduling policy. In this paper, we propose a novel binary-search-inspired technique that allows to extend timed automata models of robotic specifications with dynamic-priority schedulers. Given a number of cores, the extended models can then be checked against various real-time and behav-ioral properties, including schedulability, within the same model checking framework. Our technique is implemented in an automatic translation from a robotic framework to UPPAAL, and evaluated on a real robotic case study, where it shows a significant gain in scalability as opposed to the counting technique used in the literature.
Fichier principal
Vignette du fichier
main.pdf (1.18 Mo) Télécharger le fichier
Origine : Fichiers produits par l'(les) auteur(s)

Dates et versions

hal-02864928 , version 1 (11-06-2020)
hal-02864928 , version 2 (16-09-2020)
hal-02864928 , version 3 (15-02-2021)

Identifiants

Citer

Mohammed Foughali, Pierre-Emmanuel Hladik. Bridging the Gap between Formal Verification and Schedulability Analysis: The Case of Robotics. Journal of Systems Architecture, 2020, 111, pp.101817. ⟨10.1016/j.sysarc.2020.101817⟩. ⟨hal-02864928v3⟩
178 Consultations
275 Téléchargements

Altmetric

Partager

Gmail Facebook X LinkedIn More