Formal Specification and Verification of Autonomous Robotic Systems: A Survey

An autonomous system is an artificially intelligent entity that makes decisions in response to input, independent of human interaction. Robotic systems are physical entities that interact with the physical world. Thus, we consider an autonomous robotic system as a machine that uses Artificial Intelligence (AI), has a physical presence in and interacts with the real world. They are complex, inherently hybrid, systems, combining both hardware and software; they often require close safety, legal, and ethical consideration. Autonomous robotics are increasingly being used in commonplace-scenarios, such as driverless cars [68], pilotless aircraft [176], and domestic assistants [174, 60]. While for many engineered systems, testing, either through real deployment or via simulation, is deemed sufficient; the unique challenges of autonomous robotics, their dependence on sophisticated software control and decision-making, and their increasing deployment in safety-critical scenarios, require a stronger form of verification. This leads us towards using formal methods, which are mathematically-based techniques for the specification and verification of software systems, to ensure the correctness of, and provide sufficient evidence for the certification of, robotic systems. We contribute an overview and analysis of the state-of-the-art in formal specification and verification of autonomous robotics.