Modeling for Verification of Robotic Control Software

Robotic systems are becoming everyday more safety critical, as they started to share more space with humans in everyday life. For this reason, robots must provide strong guarantees regarding the safety of their operations. This requires to verify the software controlling the system, as well as its impact on the physical world. Approaching the problem monolithically will be unbearable for any formal verification method. For this reason, software must be verified assuming the characteristics of the physical world the system interacts with.

This seminar will present a technique to create abstract models of robotic systems, representing the point of view of the software controlling the robot. Modeling is based on the Linear Temporal Logic and models are then used to verify control software by applying model checking techniques. The modeling approach defines various abstractions for the different components and aspects represented by the models. Then, a set of safety property to be verified will be defined for the control software. Finally, the seminar introduces which abstractions must be used to verify each kind of property. The approach has been implemented in an automatic tool. Its 

application to different case studies shows the potential of such a modeling approach.

The seminar will also introduce some future steps of the work, to extend the work to tackle security, alongside safety, problems in robotic systems.