Verification of Autonomous Robots: A Roboticist’s Bottom-Up Approach - LAAS - Laboratoire d'Analyse et d'Architecture des Systèmes Accéder directement au contenu
Chapitre D'ouvrage Année : 2021

Verification of Autonomous Robots: A Roboticist’s Bottom-Up Approach

Félix Ingrand

Résumé

Autonomous robots may be one day allowed to fly or to drive around in large numbers, but this will require their makers and programmers to show that the most critical parts of their software are robust and reliable. Moreover, autonomous robots embed onboard deliberation functions. This is what makes them autonomous but opens for new challenges. There are many approaches to consider for the V&V of AR software, e.g. write high-level specifications and derive them in correct implementations, deploy and develop new or modified V&V formalisms to program robotics components, etc. One should note that learned models aside, most models used in deliberation functions are already amenable to formal V&V. Thus, we rather focus on the functional level components or modules and propose an approach that relies on an existing robotics specification and implementation framework (GenoM), in which we harness existing well known formal V&V frameworks (UPPAAL, BIP, FIACRE-TINA). GenoM was originally developed by roboticists and software engineers, who wanted to clearly and precisely specify how a reusable, portable, middleware independent, functional component should be specified and implemented. As a result, GenoM has a rigorous specification, a clear semantics of the implementation and it provides a template mechanism to synthesize code that opens the door to automatic formal-model synthesis and formal V&V (offline and online). This bottom-up approach, which starts from components implementation, is more modest than the top-down ones which aim at a larger and more global view of the problem. Yet, it gives encouraging results on real implementations on which one can build more complex high-level properties to be then verified and validated offline but also with online monitors.
Fichier principal
Vignette du fichier
paper.pdf (6.37 Mo) Télécharger le fichier
Origine : Fichiers produits par l'(les) auteur(s)

Dates et versions

hal-02927311 , version 1 (01-09-2020)
hal-02927311 , version 2 (11-03-2021)
hal-02927311 , version 3 (04-04-2021)

Identifiants

  • HAL Id : hal-02927311 , version 2

Citer

Félix Ingrand. Verification of Autonomous Robots: A Roboticist’s Bottom-Up Approach. RoboSoft: Software engineering for robotics, In press. ⟨hal-02927311v2⟩
77 Consultations
63 Téléchargements

Partager

Gmail Facebook X LinkedIn More