Skip to Main content Skip to Navigation
New interface
Preprints, Working Papers, ...

A formal toolchain for offline and run-time verification of robotics systems: This is an extended version (including the Minnie RMP440 experiment) of a paper currently under review

Silvano Dal Zilio 1 Pierre-Emmanuel Hladik 1 Félix Ingrand 2 Anthony Mallet 3 
1 LAAS-VERTICS - Équipe Verification de Systèmes Temporisés Critiques
LAAS - Laboratoire d'analyse et d'architecture des systèmes
2 LAAS-RIS - Équipe Robotique et InteractionS
LAAS - Laboratoire d'analyse et d'architecture des systèmes
3 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 robotics 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 robotics software components, which can also automatically synthesize a formal model of these components. The fact that this formal model is behaviourally equivalent to the implementation of the component is very promising. We show how we can use this formal model to prove properties both offline, for model-checking (e.g., schedulability, worst-case time, exclusivity). We also describe our approach to execute this formal model, in place of a traditional implementation, and show how this provides the opportunity to add powerful monitoring and runtime verification capabilities to the system (e.g., prevent robot damage, force landing). 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 open 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 : Tuesday, May 31, 2022 - 2:33:08 PM
Last modification on : Tuesday, October 25, 2022 - 11:58:11 AM

File

main_rob.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-03683044, version 1

Citation

Silvano Dal Zilio, Pierre-Emmanuel Hladik, Félix Ingrand, Anthony Mallet. A formal toolchain for offline and run-time verification of robotics systems: This is an extended version (including the Minnie RMP440 experiment) of a paper currently under review. 2022. ⟨hal-03683044v1⟩

Share

Metrics

Record views

28

Files downloads

6