University of Cambridge > Talks.cam > Logic and Semantics Seminar (Computer Laboratory) > RoboCert: A Formal Specification Notation for Robotic Software

RoboCert: A Formal Specification Notation for Robotic Software

Add to your list(s) Download to your calendar using vCal

If you have a question about this talk, please contact Jamie Vicary.

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.

This talk is part of the Logic and Semantics Seminar (Computer Laboratory) series.

Tell a friend about this talk:

This talk is included in these lists:

Note that ex-directory lists are not shown.

 

© 2006-2024 Talks.cam, University of Cambridge. Contact Us | Help and Documentation | Privacy and Publicity