RoboWorld: Verification of Robotic Systems with Environment in the Loop

What is it about?

Recent advances in Engineering and Artificial Intelligence promise a transformative impact on our society, as robots become ubiquitous in homes, offices, and public spaces, to facilitate and enrich our lives. Development of software for robots operating in these complex environments, however, is a challenge. Roboticists often have in mind restrictions that must be satisfied for their robots to operate well. Rarely, however, these restrictions are recorded precisely or at all. Here, we present RoboWorld, a domain-specific controlled natural language with precise semantics that can be used to define operational requirements, and environment interactions of a robot.

Featured Image

Photo by Bill Nino on Unsplash

Photo by Bill Nino on Unsplash

Why is it important?

A robot affects and is affected by its environment, so that typically its behaviour depends on features of that environment: the terrain, the presence of obstacles, and so on. To establish trustworthiness of such systems (safety, resilience, security, and so on), we need to take into account those properties. For example, whether a robot can move and reach a target, perhaps within a particular period of time, does depend on the conditions of the environment. In other words, reliable use of a robot may be restricted to certain operational conditions. With RoboWorld, we can specify those conditions using natural language, a controlled subset of English, but can still reason in the context those requirements using mathematics. A RoboWorld document gives an explicit and unambiguous specification of operational requirements of robotic systems. From these, we can take advantage of a mathematical account of the document to generate tests and simulations for the system automatically, or to prove its properties. Together, these efforts can provide evidence of trustworthiness under the given operational conditions.