A formal toolchain for offline and run-time verification of robotic systems - LAAS - Laboratoire d'Analyse et d'Architecture des Systèmes Accéder directement au contenu
Article Dans Une Revue Robotics and Autonomous Systems Année : 2023

A formal toolchain for offline and run-time verification of robotic systems

Résumé

Validation and Verification (V&V) of autonomous robotic system software is becoming a critical issue. Among the V&V techniques at our disposal, formal approaches are among the most rigorous and trustworthy ones. Yet, the level of skills and knowledge required to use and deploy formal methods is usually quite high and rare. In this paper, we describe an approach that starts from a regular, but rigorous, framework to specify and deploy robotic software components, which can also automatically synthesize a formal model of these components. We describe how we can execute the resulting formal model, in place of a traditional imple- mentation, and show how this provides the opportunity to add powerful monitoring and runtime verification capabilities to a system, e.g., to prevent collisions, or trigger an emergency landing. Since the runtime used to execute formal models is specifically designed to be faithful to their se- mantics, every execution (in the implementation) can be mapped to a trace in the specification. As a result, we can also prove many interesting properties offline, using model-checking techniques. We give several examples, such as properties about schedulability, worst-case traversal time, or mutual exclusion. We believe that having a consistent workflow, from an initial specification of our system, down to a formal, executable specification is a major advance in robotics and opens the way for verification of functional components of autonomous robots and beyond. We illustrate this claim by describing a complete example based on a genuine drone flight controller.
Fichier principal
Vignette du fichier
main_rob.pdf (4.88 Mo) Télécharger le fichier
Origine : Fichiers produits par l'(les) auteur(s)

Dates et versions

hal-03683044 , version 1 (31-05-2022)
hal-03683044 , version 2 (17-10-2022)

Identifiants

Citer

Silvano Dal Zilio, Pierre-Emmanuel Hladik, Félix Ingrand, Anthony Mallet. A formal toolchain for offline and run-time verification of robotic systems. Robotics and Autonomous Systems, 2023, 159, pp.104301. ⟨10.1016/j.robot.2022.104301⟩. ⟨hal-03683044v2⟩
174 Consultations
65 Téléchargements

Altmetric

Partager

Gmail Facebook X LinkedIn More