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

Alvaro Heiji Miyazawa; Pedro Fernando De Oliveira Salazar Ribeiro; W. Li; Ana Lucia Caneca Cavalcanti; Jonathan Ian Timmis; JAMES Charles Paul Woodcock

doi:10.1007/s10270-018-00710-z

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

Alvaro Heiji Miyazawa, Pedro Fernando De Oliveira Salazar Ribeiro, W. Li, Ana Lucia Caneca Cavalcanti, Jonathan Ian Timmis, JAMES Charles Paul Woodcock

Research output: Contribution to journal › Article › peer-review

Abstract

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.

Original language	English
Pages (from-to)	3097-3149
Number of pages	53
Journal	Software and Systems Modeling
Volume	18
Issue number	5
Early online date	24 Jan 2019
DOIs	https://doi.org/10.1007/s10270-018-00710-z
Publication status	Published - 1 Oct 2019

Bibliographical note

Keywords

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

Access to Document

10.1007/s10270-018-00710-z

Miyazawa2019_Article_RoboChartModellingAndVerificat
© The Author(s) 2019
Final published version, 3.88 MBLicence: CC BY

https://rdcu.be/bh7dI

Ana Lucia Caneca Cavalcanti
- ana.cavalcantiyork.acuk
- Computer Science - Professor
Person: Academic

1 Seminar/workshop/course

Workshop on Requirements Modelling for Cyber-Physical Systems
Woodcock, J. (Advisor)
22 Jul 2019 → 24 Jul 2019
Activity: Participating in or organising an event › Seminar/workshop/course

Cite this

@article{e0cfc1f29cd448e88f39bc34c1102c45,

title = "RoboChart: modelling and verification of the functional behaviour of robotic applications",

abstract = "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.",

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

author = "Miyazawa, {Alvaro Heiji} and {De Oliveira Salazar Ribeiro}, {Pedro Fernando} and W. Li and Cavalcanti, {Ana Lucia Caneca} and Timmis, {Jonathan Ian} and Woodcock, {JAMES Charles Paul}",

note = "{\textcopyright} The Author(s) 2019",

year = "2019",

month = oct,

day = "1",

doi = "10.1007/s10270-018-00710-z",

language = "English",

volume = "18",

pages = "3097--3149",

journal = "Software and Systems Modeling",

issn = "1619-1366",

publisher = "Springer",

number = "5",

}

TY - JOUR

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

AU - Miyazawa, Alvaro Heiji

AU - De Oliveira Salazar Ribeiro, Pedro Fernando

AU - Li, W.

AU - Cavalcanti, Ana Lucia Caneca

AU - Timmis, Jonathan Ian

AU - Woodcock, JAMES Charles Paul

N1 - © The Author(s) 2019

PY - 2019/10/1

Y1 - 2019/10/1

N2 - 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.

AB - 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.

KW - CSP

KW - Domain-specific language for robotics

KW - Formal semantics

KW - Model checking

KW - Process algebra

KW - State machines

KW - Timed properties

U2 - 10.1007/s10270-018-00710-z

DO - 10.1007/s10270-018-00710-z

M3 - Article

SN - 1619-1366

VL - 18

SP - 3097

EP - 3149

JO - Software and Systems Modeling

JF - Software and Systems Modeling

IS - 5

ER -

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

Abstract

Bibliographical note

Keywords

Access to Document

Profiles

Ana Lucia Caneca Cavalcanti

Activities

Workshop on Requirements Modelling for Cyber-Physical Systems

Cite this