Abstract
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).
| Original language | English |
|---|---|
| Article number | 26 |
| Number of pages | 46 |
| Journal | Formal Aspects of Computing |
| Volume | 35 |
| Issue number | 4 |
| DOIs | |
| Publication status | Published - 20 Nov 2023 |
Bibliographical note
Funding Information:The work reported here is funded by the Royal Academy of Engineering grant CiET1718/45, UK EPSRC grants EP/M025756/1 and EP/R025479/1, and UKRI TAS Verifiability Node EP/V026801/1. The work is also partially supported by CNPq grant 465614/2014-0, CAPES grant 88887.136410/2017-00, and FACEPE grants APQ-0399-1.03/17 and PRONEX APQ/0388-1.03/14.
Publisher Copyright:
© 2023 held by the owner/author(s). Publication rights licensed to ACM.
Keywords
- controlled natural languages
- domain-specific languages
- hybrid systems
- Model-driven engineering
- process algebra