Skip to Main content Skip to Navigation
Book section

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

Félix Ingrand 1
1 LAAS-RIS - Équipe Robotique et InteractionS
LAAS - Laboratoire d'analyse et d'architecture des systèmes
Abstract : 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.
Complete list of metadata

https://hal.laas.fr/hal-02927311
Contributor : Felix Ingrand <>
Submitted on : Sunday, April 4, 2021 - 10:32:22 AM
Last modification on : Friday, June 18, 2021 - 4:15:51 PM

File

paper.pdf
Files produced by the author(s)

Identifiers

Citation

Félix Ingrand. Verification of Autonomous Robots: A Roboticist’s Bottom-Up Approach. Software engineering for robotics, Springer, In press, 978-3-030-66493-0. ⟨10.1007/978-3-030-66494-7_8⟩. ⟨hal-02927311v3⟩

Share

Metrics

Record views

101

Files downloads

76