Journal
SOFTWARE AND SYSTEMS MODELING
Volume 18, Issue 5, Pages 3097-3149Publisher
SPRINGER HEIDELBERG
DOI: 10.1007/s10270-018-00710-z
Keywords
State machines; Formal semantics; Process algebra; CSP; Model checking; Timed properties; Domain-specific language for robotics
Categories
Funding
- EPSRC [EP/M025756/1, EP/R025479/1]
- Royal Academy of Engineering
- EPSRC [EP/R025479/1, EP/M025756/1] Funding Source: UKRI
Ask authors/readers for more resources
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.
Authors
I am an author on this paper
Click your name to claim this paper and add it to your profile.
Reviews
Recommended
No Data Available