By the same authors

From the same journal

From the same journal

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

Research output: Contribution to journalArticlepeer-review

Full text download(s)


Published copy (DOI)



Publication details

JournalSoftware and Systems Modeling
DateAccepted/In press - 21 Dec 2018
DateE-pub ahead of print - 24 Jan 2019
DatePublished (current) - 1 Oct 2019
Issue number5
Number of pages53
Pages (from-to)3097-3149
Early online date24/01/19
Original languageEnglish


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.

Bibliographical note

© The Author(s) 2019

    Research areas

  • CSP, Domain-specific language for robotics, Formal semantics, Model checking, Process algebra, State machines, Timed properties


Discover related content

Find related publications, people, projects, datasets and more using interactive charts.

View graph of relations