Formal Specification and Verification of Autonomous Robotic Systems: A Survey

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.

32 pages (in this format) resubmitted to ACM CSUR

References in corpus (8)

• Formal Verification of Obstacle Avoidance and Navigation of Ground Robots
• A Case Study on Formal Verification of Self-Adaptive Behaviors in a Decentralized System
• Symmetry Reduction Enables Model Checking of More Complex Emergent Behaviours of Swarm Navigation Algorithms
• Towards the Verification of Safety-critical Autonomous Systems in Dynamic Environments
• Developing Bug-Free Machine Learning Systems With Formal Mathematics
• A Rational Agent Controlling an Autonomous Vehicle: Implementation and Formal Verification
• Contribution to the Formal Specification and Verification of a Multi-Agent Robotic System
• Formal Specification and Analysis of Autonomous Systems under Partial Compliance

Cited by in corpus (26)

• Ethics-Based Auditing of Automated Decision-Making Systems: Intervention Points and Policy Implications
• Runtime Verification and Field-based Testing for ROS-based Robotic Systems
• Heterogeneous Verification of an Autonomous Curiosity Rover
• Situated Live Programming for Human-Robot Collaboration
• Model Predictive Robustness of Signal Temporal Logic Predicates
• A Summary of Formal Specification and Verification of Autonomous Robotic Systems
• Safety assurance of an industrial robotic control system using hardware/software co-verification
• Towards Integrating Formal Verification of Autonomous Robots with Battery Prognostics and Health Management
• Towards Compositional Verification for Modular Robotic Systems
• Using Formal Methods for Autonomous Systems: Five Recipes for Formal Verification
• Monitoring ROS2: from Requirements to Autonomous Robots
• Formal Modelling and Analysis of a Self-Adaptive Robotic System
• A Formally Verified Fail-Operational Safety Concept for Automated Driving
• Specification and Verification of Timing Properties in Interoperable Medical Systems
• A Mapping of Assurance Techniques for Learning Enabled Autonomous Systems to the Systems Engineering Lifecycle
• MacroSwarm: A Field-based Compositional Framework for Swarm Programming
• Revisiting Formal Methods for Autonomous Robots: A Structured Survey
• Modelling the Turtle Python library in CSP
• Interactive Physically-Based Simulation of Roadheader Robot
• Open Challenges in the Formal Verification of Autonomous Driving
• Explainable Software for Cyber-Physical Systems (ES4CPS): Report from the GI Dagstuhl Seminar 19023, January 06-11 2019, Schloss Dagstuhl
• Weakening Goals in Logical Specifications
• Establishing Reliable Robot Behavior using Capability Analysis Tables
• On the Expressive Power of the Normal Form for Branching-Time Temporal Logics
• Hybrid dynamical type theories for navigation
• Address Behaviour Vulnerabilities in the Next Generation of Autonomous Robots