How to Prove Your Robot Safe

VCLA will be hosting a talk by Andre Platzer on April 15, 2013.

ABSTRACT

Robots are up and coming and will be everywhere. Nowadays, robots interact more frequently with a dynamic environment outside limited manufacturing sites and they do so in close proximity with humans. That's why we don't want them to misbehave. Safety is key. But it's a difficult problem, because robots move around and how they move around is determined by complicated computer control programs. The combination of both aspects makes them cyber-physical systems.

This talk addresses the question how we can prove robots to be safe. How can we phrase what safety means? How can we model robots? And, once we have done that, how do we prove that the robot is safe?

We use hybrid system models and formal verification techniques based on differential dynamic logic to prove that the robot's control prevents collisions. We also verify safety despite location and actuator uncertainty. The approach we present is more general and has been used to verify other cyber-physical systems, including cars, trains, aircraft, and surgical robotics systems. The approach features a rich theory, which will, however, not play a major role in this talk.