Autor:
Rodríguez-Hortalá, Juan

Foto de perfil
E-mails conocidos
juan.rodriguez.hortala@gmail.com
juanrh@fdi.ucm.es
Fecha de nacimiento
Proyectos de investigación
Unidades organizativas
Puesto de trabajo
Apellidos
Rodríguez-Hortalá
Nombre de pila
Juan
Nombre
Nombres alternativos
Afiliaciones conocidas
Departamento de sistemas Informáticos y Computación. Universidad Complutense de Madrid, Spain
Independent researcher, Spain
DSIC-UCM
Páginas web conocidas
Página completa del ítem
Notificar un error en este autor

Filtros

20211
Restablecer filtros

Ajustes

Resultados de la búsqueda

Mostrando 1 - 1 de 1
  • Miniatura
    Artículo
    Verification of ROS Navigation using Maude
    Martin-Martin, Enrique; Montenegro, Manuel; Riesco, Adrián; Rodríguez-Hortalá, Juan; Rubio, Rubén. Actas de las XX Jornadas de Programación y Lenguajes (PROLE 2021), 2021-09-22.
    The Robot Operating System (ROS) is a framework for building robust software for complex robot systems in several domains. The emph{Navigation Stack} stands out among the different libraries available in ROS. This library provides a set of reusable components that developers can use to build robots with autonomous navigation capabilities. This is a critical component, as navigation failures could have catastrophical consequences for applications like self-driving cars. Here we show our work on the verification of the C++ code for the navfn planner, which is the main planner component of the Navigation Stack. We have ported the planner to a Maude specification, and validated their equivalence using differential testing techniques. For this purpose, we integrated the specification into ROS using a novel high performance Python interface for Maude. We then analyzed the Maude specification by means of model checking and functional verification techniques, using not only the built-in tools of Maude, but also a translation into Dafny, and a manual but systematic generation of verification conditions from the Maude specification. Along the way we also encountered counterexamples for some soundness properties —e.g. that paths should not collide with obstacles— and optimatility —paths should have the lowest possible cost— of the NavFn planner.