How can we guarantee robots will never cause harm? How can we prove that complicated mechanical systems, controlled by computers and programmed by people will always behave as expected, under changing conditions and in a variety of uncertain environments? How do we formalize what such behaviors are?
Guaranteeing safety, predictability and reliability of robots is crucial for the assimilation of such systems into society, be it at home or in the workplace. While every robotics researcher working with or on a robot is aware of safety issues, only recently the robotics community has begun looking at ways to either formally prove or guarantee by design different behavioral properties such as safety and correctness. The results that will be presented in the workshop combine and extend ideas from automata theory, logic, model checking, hybrid systems and control and they pave the way toward creating robotic “formal methods” – a body of work that will ultimately result in provable correct robotic systems.
This workshop brings together leading researchers in the field of robotics, together with top researchers from the formal methods and hybrid systems communities to discuss the state of the art, existing tools and challenges that must be addressed in order to create safe and reliable systems that can be proven to be correct, either by design or by verification.
The full day workshop consists of invited talks by both robotics and formal methods researchers, a tools session that will include tool demonstrations and a poster session.
This workshop is supported by the ExCape project