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 ROS Contract Language, which captures a node's FOL specification and links this contract to its implementation. RCL contracts can be automatically translated, by our tool Vanda, into executable monitors; which we use to verify 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 finish with smaller examples that illustrate other useful features of our framework.

翻译：用于安全关键工业场景的机器人系统通常依赖模块化软件架构，且日益包含自主组件。验证这些模块化机器人系统行为是否符合预期，需要能够应对（最好还能利用）这种内在模块性的方法。本文描述了一种对基于机器人操作系统（ROS）构建的机器人系统中的节点进行规约的组合方法——每个节点通过一阶逻辑（FOL）假设-保证契约进行规约，该契约将规约与ROS实现相连接。我们引入了推理规则，以促进这些节点级契约的组合，从而推导出系统级属性。此外，我们提出了一种新型领域特定语言——ROS契约语言（RCL），该语言捕获节点的FOL规约，并将此契约与其实现相连接。RCL契约可通过我们的工具Vanda自动转换为可执行监视器，我们利用这些监视器在运行时验证契约。我们通过一个参与核设施远程巡检的自主移动机器人的规约与验证实例展示了该方法，并辅以若干小型示例说明框架的其他实用特性。