Abstract

RoboCert is a collection of notations for specifying properties of robotic software. They form part of the RoboStar ecosystem, which provides graphical and textual languages for high-level modelling of robot systems at all stages of their lifecycle (design, simulation, testing, and deployment) while maintaining a rigorous foundation in verifiable mathematics and automation in the form of the RoboTool series of Eclipse plugins.

My work adds a variant of UML sequence diagrams to RoboCert, to facilitate the specification of properties sensitive to time, control flow, and causality (‘whenever the robot detects an obstacle, it will turn within 5 seconds’). In this talk I will focus on the semantics of RoboCert sequence diagrams, based on the tock-CSP process algebra. I will discuss ongoing work to develop a full semantic account of the language, based on existing work on the CSP semantics of SysML sequence diagrams. This work proceeds on three tracks: as a Java plugin (RoboTool) containing an automated CSP generator for RoboCert tools; as mathematical definitions targeted for future publication; and as a semi-formal Haskell mechanisation using Hedgehog tests to check expected properties of semantic rules.