Autor:
Riesco, Adrián

Cargando...
Foto de perfil

E-mails conocidos

ariesco@ucm.es
ariesco@fdi.ucm.es

Fecha de nacimiento

Proyectos de investigación

Unidades organizativas

Puesto de trabajo

Apellidos

Riesco

Nombre de pila

Adrián

Nombre

Nombres alternativos

Riesco, Adrian
Riesco, A.

Afiliaciones conocidas

Universidad Complutense de Madrid
Universidad Complutense de Madrid, Spain
Universidad Complutense de Madrid Madrid, Spain

Páginas web conocidas

Página completa del ítem
Notificar un error en este autor

Resultados de la búsqueda

Mostrando 1 - 2 de 2
  • 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.
  • Artículo
    A Declarative Debugger for Concurrent Erlang Programs
    Caballero, Rafael; Martin-Martin, Enrique; Riesco, Adrián; Tamarit, Salvador. Actas de las XV Jornadas de Programación y Lenguajes (PROLE 2015), 2015-09-15.
    Erlang is a concurrent language with features such as actor model concurrency, no shared memory, message passing communication, high scalability and availability. However, the development of concurrent programs is a complex and error prone task. In this paper we present a declarative debugging approach for concurrent Erlang programs. Our debugger asks questions about the validity of transitions between the different points of the program that involve message passing and/or process creation. The answers, which represent the intended behavior of the program, are compared with the transitions obtained in an actual execution of the program. The differences allow us to detect program errors and to point out the pieces of source code responsible for the bugs. In order to represent the computations we present a semantic calculus for concurrent Core Erlang programs. The debugger uses the proof trees in this calculus as debugging trees used for selecting the questions asked to the user. The relation between the debugging trees and the semantic calculus allows us to establish the soundness of the approach. The theoretical ideas have been implemented in a debugger prototype.