Architectural modelling for robotics: RoboArch and the CorteX example

Research output: Contribution to journalArticlepeer-review


The need for robotic systems to be verified grows as robots are increasingly used in complex applications with safety implications. Model-driven engineering and domain-specific languages (DSLs) have proven useful in the development of complex systems. RoboChart is a DSL for modelling robot software controllers using state machines and a simple component model. It is distinctive in that it has a formal semantics and support for automated verification. Our work enriches RoboChart with support for modelling architectures and architectural patterns used in the robotics domain. Support is in the shape of an additional DSL, RoboArch, whose primitive concepts encapsulate the notion of a layered architecture and architectural patterns for use in the design of the layers that are only informally described in the literature. A RoboArch model can be used to generate automatically a sketch of a RoboChart model, and the rules for automatic generation define a semantics for RoboArch. Additional patterns can be formalised by extending RoboArch. In this paper, we present RoboArch, and give a perspective of how it can be used in conjunction with CorteX, a software framework developed for the nuclear industry.
Original languageEnglish
Article number991637
Number of pages20
JournalFrontiers in Robotics and AI
Publication statusPublished - 28 Oct 2022

Bibliographical note

© 2022 Barnett, Cavalcanti and Miyazawa


  • software engineering
  • patterns
  • RoboStar framework
  • nuclear industry
  • verification
  • simulation
  • test
  • proof

Cite this