RoboWorld: Verification of Robotic Systems with Environment in the Loop

James Baxter, Gustavo Carvalho, Ana Cavalcanti, Francisco Rodrigues Júnior

Research output: Contribution to journalArticlepeer-review


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 languageEnglish
Article number26
Number of pages46
JournalFormal Aspects of Computing
Issue number4
Publication statusPublished - 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.


  • controlled natural languages
  • domain-specific languages
  • hybrid systems
  • Model-driven engineering
  • process algebra

Cite this