RoboCert: Property Specification in Robotics

Matt Windsor*, Ana Cavalcanti

*Corresponding author for this work

Research output: Chapter in Book/Report/Conference proceedingConference contribution


RoboStar is a toolkit for model-based development using a domain-specific notation, RoboChart, with enriched UML-like state machines and a custom component model. We present RoboCert: a novel notation, based on UML sequence diagrams, which facilitates the specification of properties over RoboChart components. With RoboCert, we can express properties of a robotic system in a user-friendly, idiomatic manner. RoboCert specifications can be existential or universal, include timing notions such as deadlines and budgets, and both safety and liveness properties. Our work is faithful to UML where it can be, but presents significant extensions to fit the robotics application needs. RoboCert comes with tooling support for modelling and verification by model checking, and formal semantics in tock-CSP, the discrete-time variant of CSP.
Original languageEnglish
Title of host publicationICFEM 2022
Subtitle of host publicationFormal Methods and Software Engineering
Number of pages18
ISBN (Electronic)9783031172441
ISBN (Print)9783031172434
Publication statusPublished - 10 Oct 2022
Event23rd International Conference on Formal Engineering Methods - Universidad Complutense de Madrid, Madrid, Spain
Duration: 24 Oct 202227 Oct 2022
Conference number: 23

Publication series

NameLecture Notes in Computer Science
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349


Conference23rd International Conference on Formal Engineering Methods
Abbreviated titleICFEM 2022
Internet address

Bibliographical note

© 2022 Springer Nature Switzerland AG. This is an author-produced version of the published paper. Uploaded in accordance with the publisher’s self-archiving policy. Further copying may not be permitted; contact the publisher for details


  • RoboChart
  • Timed properties
  • CSP
  • Sequence diagrams

Cite this