ROS-based design and synthesis of monitors for semi-formal verification of robotics applications

Starting date
March 9, 2020
Duration (months)
Computer Science, Department of Engineering for Innovation Medicine
Managers or local contacts
Pravadelli Graziano

There is a trend towards increased and higher-level autonomy in robotics. The trend is most evident in mobile robots, such as self-driving cars and Unmanned Aerial Vehicles (UAVs), but it also affects personal robotics, warehouse robots (e.g., Kuka robots), and other application domains such as medical devices.
A major impediment to efficiently developing large-scale reliable robotic infrastructure with high-level autonomy is the lack of support for systematic system verication.
What is missing is a modular approach to verify the complex and heterogeneous software applications implementing the robot's behaviour during the whole HW/SW design flow. Good design practice requires the creation of runtime monitors, which are pieces of code that can monitor key properties of the system's behavior in real-time, report any violations, and possibly enforce fail-safe behavior. Simple monitors to watch resources and detect local faults are prevalent in robotic applications. However, with the increased requirements in perception and control, current robots and autonomous systems necessitate more complex monitoring tasks during their operation. These complex monitoring tasks range from enforcing safety and security properties and ensuring the correct execution of synthesized plans, to pattern matching over sensor readings to help perception.
The goal of this project is to define a methodology to automatically generate these complex monitors from their high-level specifications and integrate them into a ROS-based design flow.


GNCS National Group for Scientific Computation INDAM
Funds: assigned and managed by the department

Project participants

Stefano Aldegheri
Research Scholarship Holders
Nicola Bombieri
Full Professor
Alessandro Farinelli
Full Professor
Paolo Fiorini
Research Assistants
Franco Fummi
Full Professor
Samuele Germiniani
Temporary Professor
Riccardo Muradore
Associate Professor
Graziano Pravadelli
Full Professor
Davide Quaglia
Associate Professor
Research areas involved in the project
Sistemi ciberfisici
Embedded and cyber-physical systems