University of Cambridge > Talks.cam > Isaac Newton Institute Seminar Series > Concurrency Meeting: CSP in Practice: Timed Verification of Robot Software

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

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

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.

Tell a friend about this talk:

This talk is included in these lists:

Note that ex-directory lists are not shown.

 

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