RoboWorld: verification of robotic systems with environment in the loop
RoboWorld: verification of robotic systems with environment in the loop
复制标题
RoboWorld：在循环环境中验证机器人系统
DOI：
10.1145/3625563
复制
发表时间：
2023
影响因子：
1
通讯作者：
Baxter J
中科院分区：
文献类型：
--
作者：
Baxter J
机器人会影响环境，也会受到环境的影响，所以它的行为通常取决于环境的特性。为了验证，我们需要形式化这些属性。对环境进行建模是非常具有挑战性的，如果不是不可能的话，但我们可以捕捉假设。在这里，我们提出了RoboWorld，一种具有过程代数语义的特定领域受控自然语言，可用于定义(a)操作需求，以及(b)机器人的环境交互。RoboWorld是RoboStar框架的一部分，用于验证机器人系统。在本文中，我们定义了RoboWorld的语法和混合语义，并说明了它在捕获操作需求、自动测试生成和证明方面的用途。我们还提供了一个支持编写RoboWorld文档的工具。由于RoboWorld是一种受控的自然语言，它补充了机器人专家可以访问的其他RoboStar符号，同时受益于形式语义来支持严格的验证（通过测试和证明）。
A robot affects and is affected by its environment, so that typically its behaviour depends on properties of that environment. For verification, we need to formalise those properties. Modelling the environment is very challenging, if not impossible, but we can capture assumptions. Here, we present RoboWorld, a domain-specific controlled natural language with a process algebraic semantics that can be used to define (a) operational requirements, and (b) environment interactions of a robot. RoboWorld is part of the RoboStar framework for verification of robotic systems. In this article, we define RoboWorld’s syntax and hybrid semantics, and illustrate its use for capturing operational requirements, for automatic test generation, and for proof. We also present a tool that supports the writing of RoboWorld documents. Since RoboWorld is a controlled natural language, it complements the other RoboStar notations in being accessible to roboticists, while at the same time benefitting from a formal semantics to support rigorous verification (via testing and proof).