Formal specification and verification of autonomous robotic systems: a survey

Autonomous robotic systems are complex, hybrid, and often safety-critical; this makes their formal specification and verification uniquely challenging. Though commonly used, testing and simulation alone are insufficient to ensure the correctness of, or provide sufficient evidence for the certification of, autonomous robotics. This paper systematically surveys formal specification and verification for autonomous robotics. It identifies and categorises the challenges posed by, the formalisms aimed at, and the formal approaches for the specification and verification of autonomous robotics. Rational agent-based systems that can explain their reasoning provide a good route for providing evidence for public trust or certification bodies, because they enable the crucial transparency that trust and certification needs. Since no one formalism is capable of adequately capturing that all aspects of a robotic system behave as expected, a focussed research effort on the combination or integration of formal methods - together with a common framework for translating between formalisms and IDE-like usability of the tools - should improve their uptake in robotic systems development, where formal verification is crucial especially at the early stages when field tests of the control software are infeasible or dangerous.