BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Concurrency Meeting:  CSP in Practice: Timed Verification of Robot
  Software - Matthew Windsor (University of York)
DTSTART:20220812T091000Z
DTEND:20220812T093500Z
UID:TALK177356@talks.cam.ac.uk
DESCRIPTION:This talk describes work done by myself and the RoboStar team 
 in York to tackle the verification of timed properties of robotic control 
 software. &nbsp\;We reduce the problem into one of concurrency reasoning\,
  where Communicating Sequential Processes is the underlying formalism. &nb
 sp\;On top of CSP\, we build domain-specific languages that present specif
 ications and implementation models in a manner that is both approachable t
 o robotics experts and suitable for use in other ways (simulation model ex
 traction\, code generation\, other formalisms\, etc.). &nbsp\;I discuss Ro
 boChart\, RoboStar's DSL for software models\, and RoboCert\, a DSL I am w
 orking on to handle specifications.
LOCATION:Seminar Room 1\, Newton Institute
END:VEVENT
END:VCALENDAR
