Formal Specification and Verification of Autonomous Robotic Systems: A Survey

TL;DR

This survey reviews the current state of formal specification and verification methods for autonomous robotic systems, highlighting challenges, formalisms, and approaches to ensure safety and correctness beyond testing.

Contribution

It provides a comprehensive overview and categorization of formal methods applied to autonomous robotics, addressing a gap in current literature.

Findings

Formal methods are increasingly applied to autonomous robotics.

Challenges include system complexity and safety-critical requirements.

Formal approaches help improve reliability and certification processes.

Abstract

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. Formal methods for autonomous robotics has received some attention in the literature, but no resource provides a current overview. This paper systematically surveys the state-of-the-art in formal specification and verification for autonomous robotics. Specially, it identifies and categorises the challenges posed by, the formalisms aimed at, and the formal approaches for the specification and verification of autonomous robotics.