RT Journal Article
T1 Verification of the ROS NavFn planner using executable specification languages
A1 Martin-Martin, Enrique
A1 Montenegro Montes, Manuel
A1 Riesco Rodríguez, Adrián
A1 Rodríguez Hortalá, Juan
A1 Rubio Cuéllar, Rubén Rafael
AB The Robot Operating System (ROS) is a framework for building robust software for complex robot systems in several domains. The Navigation Stack stands out among the different libraries available in ROS, providing a set of components that can be reused to build robots with autonomous navigation capabilities. This library is a critical component, as navigation failures could have catastrophic consequences for applications like self-driving cars where safety is crucial.Here we devise a general methodology for verifying this kind of complex systems by specifying them in different executable specification languages with verification support and validating the equivalence between the specifications and the original system using differential testing techniques. The complex system can then be indirectly analyzed using the verification tools of the specification languages like model checking, semi-automated functional verification based on Hoare logic, and other formal techniques. In this paper we apply this verification methodology to the NavFn planner, which is the main planner component of the Navigation Stack of ROS, using Maude and Dafny as specification languages. We have formally proved several desirable properties of this planner algorithm like the absence of obstacles in the planned path. Moreover, we have found counterexamples for other concerns like the optimality of the path cost.
PB Elsevier
SN 2352-2216
YR 2023
FD 2023-04
LK https://hdl.handle.net/20.500.14352/73028
UL https://hdl.handle.net/20.500.14352/73028
LA spa
NO CRUE-CSIC (Acuerdos Transformativos 2023)
NO Agencia Estatal de Investigación
NO Ministerio de Economía y Competitividad
NO Ministerio de Universidades
NO Comunidad de Madrid
DS Docta Complutense
RD 9 abr 2025