RoboCert: A Formal Specification Notation for Robotic Software

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

• Matthew Windsor, University of York
• Friday 09 June 2023, 14:00-15:00
• SS03, Computer Laboratory.

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.

This talk is included in these lists:

• All Talks (aka the CURE list)
• Cambridge talks
• Computing and Mathematics
• Department of Computer Science and Technology talks and seminars
• Interested Talks
• Logic and Semantics Seminar (Computer Laboratory)
• SS03, Computer Laboratory
• School of Technology
• Trust & Technology Initiative - interesting events
• bld31
• yk373's list

Note that ex-directory lists are not shown.