A formal toolchain for offline and run-time verification of robotics systems - LAAS - Laboratoire d'Analyse et d'Architecture des Systèmes Accéder directement au contenu
Pré-Publication, Document De Travail Année : 2022

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

Résumé

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.
Fichier principal
Vignette du fichier
main_rob.pdf (7.69 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

  • HAL Id : hal-03683044 , version 1

Citer

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⟩
174 Consultations
65 Téléchargements

Partager

Gmail Facebook X LinkedIn More