A Summary of Formal Specification and Verification of Autonomous Robotic Systems

TL;DR

This paper reviews the current state of formal specification and verification methods for autonomous robotic systems, emphasizing their importance for safety-critical applications and highlighting recent research contributions.

Contribution

It provides a comprehensive overview of recent advancements in formal methods applied to autonomous robotics, filling a gap in existing literature.

Findings

Formal methods are increasingly applied to autonomous robotics

Testing and simulation are insufficient for certification

Recent research advances improve safety assurance

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 have received some attention in the literature, but no resource provides a current overview. This short paper summarises the contributions of Luckcuck 2019, which surveys the state-of-the-art in formal specification and verification for autonomous robotics.