Concurrency Meeting: CSP in Practice: Timed Verification of Robot Software

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

• Matthew Windsor (University of York)
• Friday 12 August 2022, 10:10-10:35
• Seminar Room 1, Newton Institute.

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

VSO2 - Verified software

This talk describes work done by myself and the RoboStar team in York to tackle the verification of timed properties of robotic control software.  We reduce the problem into one of concurrency reasoning, where Communicating Sequential Processes is the underlying formalism.  On top of CSP , we build domain-specific languages that present specifications and implementation models in a manner that is both approachable to robotics experts and suitable for use in other ways (simulation model extraction, code generation, other formalisms, etc.).  I discuss RoboChart, RoboStar’s DSL for software models, and RoboCert, a DSL I am working on to handle specifications.

This talk is part of the Isaac Newton Institute Seminar Series series.

This talk is included in these lists:

• All CMS events
• Featured lists
• INI info aggregator
• Isaac Newton Institute Seminar Series
• School of Physical Sciences
• Seminar Room 1, Newton Institute
• bld31

Note that ex-directory lists are not shown.