BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:RoboCert: A Formal Specification Notation for Robotic Software - M
 atthew Windsor\, University of York
DTSTART:20230609T130000Z
DTEND:20230609T140000Z
UID:TALK202099@talks.cam.ac.uk
CONTACT:Jamie Vicary
DESCRIPTION:RoboCert is a collection of notations for specifying propertie
 s of robotic software.  They form part of the RoboStar ecosystem\, which p
 rovides 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 math
 ematics and automation in the form of the RoboTool series of Eclipse plugi
 ns.\n\nMy work adds a variant of UML sequence diagrams to RoboCert\, to fa
 cilitate 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 RoboC
 ert sequence diagrams\, based on the tock-CSP process algebra.  I will dis
 cuss ongoing work to develop a full semantic account of the language\, bas
 ed 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 t
 argeted for future publication\; and as a semi-formal Haskell mechanisatio
 n using Hedgehog tests to check expected properties of semantic rules.
LOCATION:SS03\, Computer Laboratory
END:VEVENT
END:VCALENDAR