Cookies Policy
The website need some cookies and similar means to function. If you permit us, we will use those means to collect data on your visits for aggregated statistics to improve our service. Find out More
Accept Reject
  • Menu

InfoBlender Webinar

Verification of system-wide safety properties of ROS applications



Robots are currently deployed in safety-critical domains but proper techniques to assess the functional safety of their software are yet to be adopted. This is particularly critical in ROS, where highly configurable robots are built by composing third-party modules. To promote adoption, we advocate the use of lightweight formal methods, automatic techniques with minimal user input and intuitive feedback.
This paper proposes a technique to automatically verify system-wide safety properties of ROS-based applications at static time. It is based in the formalization of ROS architectural models and node behaviour in Electrum, over which system-wide specifications are subsequently model checked. To automate the analysis, it is deployed as a plug-in for HAROS, a framework for the assessment of ROS software quality aimed at the ROS community. The technique is evaluated in a real robot with positive results.



Nuno Macedo is an Assistant Professor of the Faculty of Engineering of University of Porto (FEUP) and a researcher at the High-Assurance Software Laboratory (HASLab) of INESC TEC. He focuses on developing, teaching and applying formal techniques for software engineering with the goal of promoting the development of dependable software. His main research interest is in trustworthy software design, particularly approaches based on lightweight formal methods backed by model checking and model finding. He has also tailored such techniques for the robotics domain to promote the development of safe robotics software.


Please register here until October 28, in order to have access to the link for the Zoom session. The slides are available here.



  • Start

    29th October 2020
  • Start Hour

  • Promoters

    HASLab, INESC TEC and University of Minho
  • Country

  • Local