Close menu


Sunderland Repository records the research produced by the University of Sunderland including practice-based research and theses.

RoboChart: modelling and verification of the functional behaviour of robotic applications

Miyazawa, Alvero, Ribero, Pedro, Cavalcanti, Anna, Timmis, Jonathan and Woodcock, Jim (2019) RoboChart: modelling and verification of the functional behaviour of robotic applications. Software Systems and Modelling, 18. pp. 3097-3149.

Item Type: Article


Robots are becoming ubiquitous: from vacuum cleaners to driverless cars, there is a wide variety of applications, many with potential safety hazards. The work presented in this paper proposes a set of constructs suitable for both modelling robotic applications and supporting verification via model checking and theorem proving. Our goal is to support roboticists in writing models and applying modern verification techniques using a language familiar to them. To that end, we present RoboChart, a domain-specific modelling language based on UML, but with a restricted set of constructs to enable a simplified semantics and automated reasoning. We present the RoboChart metamodel, its well-formedness rules, and its process-algebraic semantics. We discuss verification based on these foundations using an implementation of RoboChart and its semantics as a set of Eclipse plug-ins called RoboTool.

Full text not available from this repository.

More Information

Depositing User: Jonathan Timmis


Item ID: 11852
Identification Number:
Official URL:

Users with ORCIDS

Catalogue record

Date Deposited: 24 Mar 2020 14:07
Last Modified: 17 Jul 2020 13:54


Author: Alvero Miyazawa
Author: Pedro Ribero
Author: Anna Cavalcanti
Author: Jonathan Timmis
Author: Jim Woodcock

University Divisions

Faculty of Technology > School of Computer Science


Computing > Software Engineering

Actions (login required)

View Item (Repository Staff Only) View Item (Repository Staff Only)