A Compositional Approach to Verifying Modular Robotic Systems

Robotic systems used in safety-critical industrial situations often rely on modular software architectures, and increasingly include autonomous components. Verifying that these modular robotic systems behave as expected requires approaches that can cope with, and preferably take advantage of, this inherent modularity. This paper describes a compositional approach to specifying the nodes in robotic systems built using the Robotic Operating System (ROS), where each node is specified using First-Order Logic (FOL) assume-guarantee contracts that link the specification to the ROS implementation. We introduce inference rules that facilitate the composition of these node-level contracts to derive system-level properties. We also present a novel Domain-Specific Language, the RCL, which captures a node's FOL specification and links this contract to its implementation. ROS Contract Language (RCL) contracts can be automatically translated, by our tool Vanda, into executable monitors; which we use to enforce the contracts at runtime. We illustrate our approach through the specification and verification of an autonomous rover engaged in the remote inspection of a nuclear site, and examples focussing on the specification and verification of individual nodes.