A Framework for Verifying the Collision Freeness of Collaborative Robots (Work in Progress)
摘要
Collision avoidance is a major problem when robotic devices are being deployed to perform complex collaborative tasks. We present a vision for a framework that makes it convenient to program collaborative robots and to verify that their behaviour is collision-free. It consists of a domain-specific language that is shallowly embedded in the ROS (Robot Operating System) framework and a translation into a programming language that is deeply embedded in the Isabelle/HOL theorem prover.