A Verifiable and Correct-by-Construction Controller for Robots in Human Environments
Résumé
With the increasing use of domestic and service robots alongside humans, it is now becoming crucial to be able to verify whether robot-software is safe, dependable, and correct. Indeed, in the near future it may well be necessary for robot-software developers to provide safety certifications guaranteeing, e.g. that a hospital nursebot will not move too fast while a person is leaning on it, that the arm of a service robot will not unexpectedly open its gripper while holding a glass, or that there will never be a software deadlock while a robot is navigating in an office. To this end, we have provided a framework and software engineering methodology for developing safe and dependable real-world robotic architectures, with a focus on the functional level--the lowest level of a typical layered robotic architecture--which has all the basic action and perception capabilities such as image processing, obstacle avoidance, and motion control. Unlike past work we address the formal verification of the functional level, which allows providing guarantees that it will not do steps leading to undesirable/disastrous outcomes.