Skip to Main content Skip to Navigation
New interface
Journal articles

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

Silvano Dal Zilio 1 Pierre-Emmanuel Hladik 2 Félix Ingrand 3 Anthony Mallet 4 
1 LAAS-VERTICS - Équipe Verification de Systèmes Temporisés Critiques
LAAS - Laboratoire d'analyse et d'architecture des systèmes
3 LAAS-RIS - Équipe Robotique et InteractionS
LAAS - Laboratoire d'analyse et d'architecture des systèmes
4 LAAS-IDEA - Service Informatique : Développement, Exploitation et Assistance
LAAS - Laboratoire d'analyse et d'architecture des systèmes
Abstract : 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.
Complete list of metadata

https://hal.laas.fr/hal-03683044
Contributor : Felix Ingrand Connect in order to contact the contributor
Submitted on : Monday, October 17, 2022 - 3:43:39 PM
Last modification on : Tuesday, November 22, 2022 - 1:41:39 PM

File

main_rob.pdf
Files produced by the author(s)

Identifiers

Citation

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⟩

Share

Metrics

Record views

28

Files downloads

6