Formal Specification and Verification of Autonomous Robotic Systems: A Survey

2 min read

A systematic survey of formal specification and verification for autonomous robots, covering 2007 to 2018. The authors screened 156 papers, kept 63 as in scope, and sort them by the challenges they face (external: modelling the environment, producing certification evidence; internal: agent-based, multi-robot and reconfigurable systems), by formalism, and by verification approach.

Findings

  • Model checking dominates: 32 of the 63 core papers use it, against 3 for theorem proving and 3 for runtime monitoring. State-transition systems are the most common way to model a robot and temporal logics the most common way to write properties.
  • Runtime monitors are presented as a way around verifying a full, complex model: the monitor is simpler than the robot, so it is easier to verify, and it narrows the gap between model and world. The authors also say runtime monitoring cannot guarantee all behaviours beforehand and is usually treated as a step after static verification.
  • On swarms: state-space explosion blocks direct model checking, and a proof for n robots says nothing about n plus or minus one. They cite Winfield and Nembrini’s finding that a partially failed robot (working except for its wheels) was worse for the swarm than a dead one, because it anchored the swarm in place.
  • Open problems they name: no guidance on choosing a formalism, poor interoperability between tools, few methods that carry a verified model through to running code (the “last link”), and little sharing of models and realistic case studies.

Limits

  • Ten-year window and a Google Scholar search; the authors list both as threats to validity and mitigate with snowballing.
  • Scope is software and decision logic. Physics, materials and the continuous parts are mostly excluded, and so is security.
  • Written before the wave of learned components and ROS 2, so neural perception and LLM planners do not appear.

Relevance

It surveys the field for a robotics reader and finds that almost nobody in the core set ran a verified monitor on a real robot. Robot-side runtime verification since then includes ROSMonitoring, RoboChart and Caldas et al.. The partial-failure observation is the Byzantine problem in physical form; see runtime monitoring, multi-robot systems and robust robotics.