PaperlayerView exact revision on arXiv

Source-linked AI summary

Formal Specification and Verification of Autonomous Robotic Systems: A Survey

Matt Luckcuck, Marie Farrell, Louise Dennis, Clare Dixon, Michael Fisher

arXiv:1807.00048v3cs.FLcs.RO

TL;DR

Autonomous robotic systems combine AI, physical interaction, hardware, and software in settings where testing and simulation alone may not establish correctness or certification evidence. This survey systematically analyses the literature’s challenges, formalisms, and verification approaches, finding dominant use of model checking while identifying unresolved integration and complexity limitations.

  • Problem

    Autonomous robotics lacks a current overview of how formal methods address its complex, hybrid, and safety-critical specification and verification challenges.

  • Method

    The paper systematically surveys and categorises challenges, formalisms, tools, and formal verification approaches in the literature on autonomous robotics.

  • Results

    Model checking is the most popular verification approach, while temporal logics and state-transition systems dominate robotic-system specifications.

  • Takeaways & Limitations

    The survey identifies environmental modelling, certification and trust evidence, agent-based systems, multi-robot systems, and adaptive or reconfigurable systems as central research challenges.

  • Takeaways & Limitations

    Current formal methods can be computationally and usability-wise complex, particularly when modelling complex physical environments.

Abstract

from arXiv · show

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.

1 Introduction, Methodology and Related Work

The survey addresses formal specification and verification for autonomous robotic systems, which combine AI, physical interaction, hardware, and software in safety-critical settings. It defines its scope and research questions, surveys recent literature, and distinguishes related reviews.

  • Scope: Autonomous robotic systems use AI, have physical presence, and interact with the real world while combining hardware and software.The survey also notes their safety, legal, and ethical considerations.
  • Motivation: Testing and simulation alone do not reliably establish correctness or provide sufficient certification evidence for autonomous robotics.The survey therefore motivates mathematically based formal methods for specification and verification.
  • Contribution: The survey contributes an overview and analysis of the state of the art in formal specification and verification of autonomous robotics.It covers challenges, formalisms, approaches, and future directions.
  • Methodology: The review investigates challenges, current formalisms, tools and approaches, and limitations or developing solutions in the literature.These questions structure the survey’s analysis.
  • Methodology: The search surveyed 156 papers, found 63 in scope, and restricted publication years to 2007–2018.The search used specified queries, five Google Scholar pages, and snowballing to reduce omissions.
  • Related Work: Related surveys focus on safety-critical robotics, domain-specific modelling languages, autonomous software, self-adaptive systems, or intelligent swarms rather than the full scope here.The survey positions itself as a broader formal-specification and verification review.

2 General Software Engineering Techniques for Robotic Systems

Robotic engineering uses middleware, DSLs, graphical notations, and model-driven approaches to structure development and communication. These techniques support modularity and understanding, while formal languages provide unambiguous semantics and whole-program reasoning.

  • Middleware Architectures: Middleware frameworks use communicating components or nodes and provide flexible interfaces to robotic hardware.Common examples include ROS, OPRoS, OpenRTM, Orocos, and GenoM.
  • Middleware Architectures: Middleware soundness is often assumed, but heterogeneous and parametrised systems make guaranteeing correct robot behaviour challenging.This assumption is important to trust in the robotic system.
  • Testing and Simulation: Testing and simulation examine useful behaviours, including statistically unlikely situations, but cover only part of program state space and can be time-consuming or dangerous.Field testing may also endanger people and hardware.
  • Domain Specific Languages: Robotics DSLs mainly capture architectures and mature subdomains, while relatively few target emerging subdomains or runtime use.The survey also describes DeRoS for robot safety rules and corrective actions.
  • Graphical Notations: Graphical notations support robotic software design, communication, and visualisation across distinct engineering disciplines.Statecharts underpin several executable graphical notations.
  • MDE/XML: Model-driven approaches translate high-level models into platform-specific robotic code or component models.Examples include AutomationML-to-ROS mappings, the BRICS Component Model, and MontiArcAutomaton.
  • Discussion: Formal languages provide unambiguous semantics and enable reasoning about the whole program rather than only selected behaviours.The section presents this as a distinction from less formal approaches.

3 External Challenges of Autonomous Robotic Systems

External verification challenges arise from modelling physical environments and supplying adequate certification and trust evidence. The literature uses layered, probabilistic, monitoring, and simulation-based strategies, but reality gaps, unknown environments, ethical cases, and model complexity remain significant constraints.

  • Overview: External challenges concern modelling the robotic system’s physical environment and verifying behaviour within it, independently of internal design.Real-world interactions can significantly affect safety.
  • Certification and Trust: Certification and trust evidence requirements differ across regulated domains and domestic or care settings, where safety and public perceptions must both be addressed.Pilotless-aircraft regulation remains under development, while domestic adoption can be hampered by insufficient trust and safety assurance.
  • Physical Environment: Autonomous robots face unstructured environments, imperfect sensors and motors, degraded components, and partial knowledge of their surroundings.These conditions complicate formal modelling and verification.
  • Physical Environment: Robotic architectures commonly separate hardware control, middleware, and upper-level decision-making to combine discrete computation with continuous environments.Middleware examples include ROS and GenoM.
  • Physical Environment: Assuming a static, known environment can be infeasible when objects move unpredictably or the robot must discover the environment.Such assumptions may limit model effectiveness.
  • Physical Environment: Of 33 field-test bugs, low-fidelity simulation reproduced 32, leaving only one unreproduced.The cited study examined whether low-fidelity simulation could reproduce field-test bugs.
  • Physical Environment: Probabilistic models represent dynamic and uncertain environments, but model checking still depends on encoded probabilities and may miss unforeseen detrimental situations.PRISM is used for both the robot and probabilistic environmental behaviour in one domestic-assistant example.
  • Certification and Trust: Ethical reasoning remains difficult because existing approaches may not address situations in which no ethical choice is available.The survey notes limited consideration of this case.

4 Internal Challenges of Autonomous Robotic Systems

The survey identifies agent-based, multi-robot, and reconfigurable systems as internal challenges for formally specifying and verifying autonomous robotics. These challenges involve modelling autonomous reasoning, collective behaviour, fault tolerance, adaptation, and changing environments.

  • Agent-based systems: Agent-based systems encapsulate autonomous decision-making and can model interactions with other actors and the environment.BDI agents and related implementations have been verified in aircraft, vehicle-platooning, multi-agent, and spacecraft applications.
  • Multi-robot systems: Multi-robot systems require behavioural requirements to be considered at both individual-robot and whole-system levels.The survey distinguishes swarms, whose robots exhibit similar behaviour, from teams, whose robots may behave distinctly.
  • Multi-robot systems: Swarm robustness arises from simple parallel robots operating in a fully distributed way with high redundancy, but partial robot failure can be more problematic than total failure.Research also seeks the minimum number of functioning robots required for mission completion by injecting faults and checking temporal-epistemic properties.
  • Multi-robot systems: No single formalism was sufficient for specifying and verifying emergent swarm behaviour; a blend of specialised formalisms provided the best approach.The compared formalisms were CSP, WSCCS, Unity Logic, and X-Machines.
  • Reconfigurable systems: Reconfigurable systems must sense changes in requirements or the physical environment and decide how to reconfigure while maintaining fault tolerance.This is particularly important for safety-critical robots operating in hazardous or isolated environments.
  • Summary: The survey groups its internal specification and verification challenges into agent-based, multi-robot, and reconfigurable systems.These categories describe challenges related to how autonomous robotic systems are designed and built.

5 Formalisms for Robotic Systems

The survey reviews the formalisms used to specify robotic systems and the properties checked about them. It finds that systems are usually represented as state-transition systems, while properties are typically expressed in logic, especially temporal logic.

  • Overview: The survey categorises formalisms used to specify robotic systems and the properties checked about them.Displaying both sides exposes links between formalisms and potential gaps for tool development.
  • Overview: Robotic systems were normally specified as state-transition systems, with properties expressed using a logic, typically temporal logic.Examples of other categories include the relax requirements language and Quartz with the Averest framework.
  • Verification tools: The formal verification tools identified in the survey include several tools for properties specified in temporal logic, such as Uppaal and PRISM.The number of temporal-logic tools is consistent with the prevalence of temporal logic among the reviewed formalisms.
  • Categories: The survey organises the reviewed formalisms into set-based formalisms, automata, logics, process algebras, ontologies, and other formalisms.The section separately discusses temporal, dynamic, and other logics.

5.1 Set-Based Formalisms

Set-based formalisms such as the B-Method and Z represent systems through set-theoretic data structures. The survey describes their use for self-adaptation, runtime monitoring, and probabilistic reconfiguration.

  • Set-based formalisms: Set-based formalisms such as the B-Method and Z specify systems through set-theoretic representation and manipulation of data.They are well suited to complicated data structures but usually provide limited features for capturing behaviour.
  • Tool context: The surveyed formal verification tools include multiple tools, with some approaches selecting different tools for different system components.This tool diversity is documented for the core set of 63 surveyed papers.
  • Self-adaptation: FORMS provides a Z-based reference model for arbitrary self-adaptive systems and can support type checking, visualisation, and test-case generation.The model is intended to be used with existing tools to analyse whether adaptations are valid.
  • Runtime monitoring: A Z specification, animated with the Jaza animator and compared with a running Java program through jdb, supports runtime monitoring of a robotic assembly system.The approach was demonstrated on a system designed to build robots for NASA’s ANTS project.
  • Reconfiguration: Combining Event-B with probabilistic properties supports deriving reconfigurable architectures for an on-board satellite system.PRISM is used to check reconfiguration models for both refinement-based derivation and probabilistic assessment.

5.2 State-Transition Formalisms

State-transition formalisms specify robotic behaviour through states and transitions, including timed and probabilistic variants. The survey describes their use for deadlock analysis, task planning, middleware verification, mission modelling, and probabilistic autonomy.

  • State-transition systems: Petri Nets, FSMs, and FSAs specify behaviour as state-transition systems, with extensions for time and probabilistic transitions.These models can be checked for properties such as deadlock freedom or supplied to verification tools.
  • Petri Nets: Petri Nets model reactive-agent architectures, robot plans, task plans, environments, actions, and multi-robot roles.Analyses include deadlock freedom and resource usage, while goal markings represent desired plan results.
  • Timed automata: Timed automata model ROS communication and decentralised traffic monitoring, enabling verification of safety, liveness, invariants, and correctness properties.The ROS model includes low-level information such as queue sizes and timeouts.
  • Finite-state models: Finite-state robot models combined with a Gaussian environment model are translated into MissionLab’s PARS process algebra.The environment model is based on a probability distribution of obstacle positions.
  • Probabilistic models: An APFSM extends a probabilistic finite-state machine with a weight function mapping weights onto actions, making it a discrete-time Markov chain.The formalism models autonomous behaviour and is verified with PRISM for a pilotless aircraft on a foraging mission.

5.3 Logics

Logics are prominent formalisms for specifying and verifying autonomous robotic systems, especially temporal logics for dynamic, probabilistic, swarm, software-framework, and ethical properties. The surveyed work also includes dynamic, first-order, agent, and domain-specific logics, often connected to model checking, synthesis, or runtime monitoring.

  • Temporal logics: Temporal logics are the second most prevalent formalism, with LTL, CTL, probabilistic extensions, dynamic logics, and other logic varieties represented.Temporal logics specify properties over linear or branching time, while PTL and PCTL add probability.
  • Safety and assurance: Temporal logic supports safety, certification, and trust cases, including autonomous aircraft rules, domestic-assistant safety models, and dependable swarm properties.Verification results for domestic-assistant rules and environment models improve confidence in high-level decision making.
  • Other logics: Other logic-based approaches cover ethical BDI reasoning, motion-plan synthesis, framework verification, hybrid-system proofs, and domain-specific robot behaviour.Examples include ETHAN with AJPF, μ-calculus and LTL synthesis, dL with KeYmaera, QdL for surgical robots, and Readylog for football tactics.
  • Swarm robotics: A swarm specification language combines region-graph environments, region propositions, and separate macroscopic and microscopic LTL properties to synthesize decentralised controllers.This explicitly represents both whole-swarm and individual-robot behaviour.
  • Other logics: Some surveyed approaches keep specifications local to agents, model distributed robotic systems with Klaim variants, or use logics that were too uncommon for separate categories.Local specifications may be checked for mutual satisfiability, while sparse dependencies are assumed for scalability.
  • Probabilistic logics: Probabilistic model checking supports swarm and robotic-agent verification, using PCTL with PRISM for counting abstractions, design-time checking, and runtime monitoring.Counting abstraction reduces the state space for homogeneous swarms, while agent models may use DTMCs or MDPs.

5.4 Process Algebras

Process algebras specify system behaviour through events and process interactions, making them suitable for concurrent robotic systems. The surveyed approaches combine process algebra with safety and liveness checking, stochastic analysis, timed modelling, graphical tools, and environmental models.

  • Process-algebra foundations: Process algebras define system behaviour through events and process interactions and are well suited to concurrent systems, but seldom capture probabilistic behaviour.They can represent discrete time, although probabilistic behaviour is uncommon.
  • Multi-agent systems: πADL combines FSP and π calculus with ADL to specify multi-agent safety and liveness properties and check agent programs and architectures against them.FSP properties are transformed into labelled-transition systems before checking.
  • Swarm robotics: Bio-PEPA models microscopic swarm behaviour while supporting multiple analysis methods, including stochastic simulation and statistical model checking.One model represents three-robot foraging teams that vote between long and short paths.
  • Timed modelling and tools: RoboChart gives timed state machines formal CSP semantics, while RoboTool supports graphical construction, translation, and automated checking with FDR.RoboTool generates assertions for deadlock, livelock, timelock, and nondeterminism.
  • Timed modelling and tools: CSP+T maps UML-RT real-time subsystems to parallel process-algebraic compositions, while MissionLab translates robot and environment models into PARS for behavioural checking.MissionLab represents robot behaviour with FSA and the environment with a Gaussian model before translation.

5.5 Ontologies

Ontologies provide formal domain vocabularies for concepts, properties, relationships, and axioms, enabling reasoning and knowledge reuse in autonomous robotics. Applications include environment and action modelling, human-robot interaction, personal assistants, and manufacturing reconfiguration, but tool support is limited.

  • Ontology foundations: Ontologies formally specify domain concepts, properties, relationships, and axioms, enabling reasoning that can infer new information.They function as structured bodies of domain knowledge and shared vocabularies.
  • Robotics applications: In autonomous robotics, ontologies describe environments and actions, support domain-knowledge reuse, and capture elements of human-robot interaction.The survey found little evidence of available tool support for these uses.
  • Robotics applications: The IEEE-RAS working group published ontology4 to formally specify shared concepts within robotics and automation.This provides a shared ontology for the robotics and automation domains.
  • Robotics applications: KnowRob represents knowledge in OWL and integrates encyclopaedic knowledge, environment models, action reasoning, and human observations with ROS.OWL-based manufacturing knowledge has also been used to enable reconfiguration without human intervention.

5.6 Other Formalisms

Other surveyed formalisms and frameworks support either system specification or property specification, rather than both, and include agent model checking, synchronous languages, BIP, controller synthesis, and runtime-relaxable requirements.

  • Scope of other formalisms: The surveyed “other” formalisms generally specify either the robotic system or the properties checked, not both.This distinguishes them from approaches that jointly model systems and verification properties.
  • Agent and synchronous frameworks: AJPF model-checks BDI agent programs written in GWENDOLEN against temporal-logic properties after translating them into an internal representation.Several surveyed robotic-agent studies use this framework.
  • Agent and synchronous frameworks: Averest verifies safety properties of Quartz models, where the synchronous language represents parallel execution and nondeterministic choice.The properties are specified in μ-calculus.
  • BIP and synthesis: BIP uses finite-state machines for system specification, D-Finder for deadlock and safety checking, RV-BIP for runtime monitoring, and synthesis for robotic software generation.The framework has been applied to robotic software verification and runtime specification checking.
  • BIP and synthesis: Regular-expression task specifications can be synthesized into finite-state-automaton controllers for robotic teams’ communication strategies.These approaches target behavioural properties that the team must exhibit.
  • Adaptive requirements: relax expresses requirements for dynamic self-adaptive systems using structured natural language, Boolean expressions, and temporal fuzzy-logic semantics.Its requirements may be relaxed at runtime.

5.7 Summary of Formalisms for Robotic Systems

The survey finds more studies specifying robotic systems than their properties, with state-transition systems and temporal logics dominating the literature. Model-checkers are the most used verification tools, but tool diversity can hinder model sharing and extension.

  • 56 studies specify robotic systems, compared with 41 specifying properties to be checked.
  • State-transition systems are the most numerous formalisms for system specification, while temporal logics are most numerous for specifying properties.
  • Model-checkers are the most used formal verification tools in the surveyed literature.
  • Different model-checkers capture features such as time or probability, but this variety may challenge the sharing and extension of formal models.

6 Formal Verification Approaches for Robotics

The survey covers model-checking, theorem proving, runtime monitoring, integrated formalisms, and frameworks for verifiable robotic software. Model-checking dominates because it is automatic and comparatively easy to explain, while state explosion, specialist tool knowledge, runtime incompleteness, and integration difficulties remain important constraints.

  • 6.1 Model-Checking: Model-checking is the most widely used verification approach for robotic systems, spanning temporal logics, process algebras, and programs.
  • 6.1 Model-Checking: Timed and probabilistic model-checkers support timing constraints and physical-environment uncertainty, which can improve confidence in verification results.
  • 6.1 Model-Checking: State explosion can cripple model-checking efforts, requiring careful selection of input models and properties.
  • 6.1 Model-Checking: Model-checking can incrementally synthesize motion plans and revise motion controllers through repeated checking and synthesis.
  • 6.1 Model-Checking: Model-checking is flexible across concurrent, timed, and probabilistic formalisms, but model-specific crafting increases modelling time and reduces portability.
  • 6.2 Theorem Proving: Theorem proving produces formal correctness proofs that can provide evidence for certification, but these approaches have received limited attention because their tools are harder to master.
  • 6.3 Runtime Monitoring: Runtime monitors verify specified properties by comparing system events with expected behaviour and triggering mitigation, but cannot guarantee all behaviours beforehand.
  • 6.4 Integrated Formal Methods: RoboChart integrates CSP with graphical timed state machines, while holistic integration of diverse formalisms remains an open problem.

7 Conclusion

The survey synthesizes formal specification and verification research for autonomous robotics, identifying core challenges, prominent formalisms, adoption barriers, and open integration problems. It also points to future directions including interoperable tools, clearer method selection, and stronger links between specifications and executable code.

  • Challenges: The survey distinguishes external challenges—environment modelling and certification evidence—from internal challenges involving agent-based, multi-robot, adaptive, and reconfigurable systems.It identifies reconfigurability as important for safely deploying robots in hazardous environments, while noting that substantially more work is needed.
  • Formal methods: Temporal logics, state-transition systems, and model-checkers are the most prominent formalisms and approaches in the surveyed literature from the past decade.The survey speculates that abstraction supports early development and model-checking is comparatively easy to explain to stakeholders.
  • Limitations: Formal-method adoption remains limited by perceptions of added complexity and development time, as well as by inadequate tooling, despite examples of industrial use.These concerns are described as long-standing rather than newly emerging.
  • Limitations: Interoperability remains an open problem because models and specifications for similar components can be incompatible and locked into particular tools.The survey suggests a common framework for translating between, relating, or integrating formalisms and tools.
  • Future directions: The survey finds limited guidance for selecting a suitable formal method, with its table offering some guidance while leaving detailed analysis for future work.Method selection is therefore identified as an unresolved research direction rather than a completed contribution.
  • Future directions: Few robotics examples translate formal specifications into runnable code, and the relationship between generated code and the original model is often unclear.The survey links this last-link problem to the need for formal underpinning and greater open sharing of models, code, and realistic case studies.
Loading 1807.00048v3…