Projects per year
Abstract
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 language | English |
---|---|
Title of host publication | ICFEM 2022 |
Subtitle of host publication | Formal Methods and Software Engineering |
Publisher | Springer |
Pages | 386-403 |
Number of pages | 18 |
ISBN (Electronic) | 9783031172441 |
ISBN (Print) | 9783031172434 |
DOIs | |
Publication status | Published - 10 Oct 2022 |
Event | 23rd International Conference on Formal Engineering Methods - Universidad Complutense de Madrid, Madrid, Spain Duration: 24 Oct 2022 → 27 Oct 2022 Conference number: 23 http://maude.ucm.es/ICFEM22/ |
Publication series
Name | Lecture Notes in Computer Science |
---|---|
Publisher | Springer |
Volume | 13478 |
ISSN (Print) | 0302-9743 |
ISSN (Electronic) | 1611-3349 |
Conference
Conference | 23rd International Conference on Formal Engineering Methods |
---|---|
Abbreviated title | ICFEM 2022 |
Country/Territory | Spain |
City | Madrid |
Period | 24/10/22 → 27/10/22 |
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 detailsKeywords
- RoboChart
- Timed properties
- CSP
- Sequence diagrams
Projects
- 1 Finished
-
UK Trustworthy Autonomous Systems Verifiability Node
Cavalcanti, A. L. C. (Principal investigator) & Woodcock, J. (Co-investigator)
1/11/20 → 31/10/24
Project: Research project (funded) › Research