Automated Compositional Verification for Robotic State Machines using Isabelle/HOL

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract

RoboChart is a graphical language for model-based engineering of robotic systems, in the style of UML and SysML. It contains notations for data structures, system architecture, and the behaviour of individual robotic controllers using state machines. Crucially, RoboChart has a formal semantics in the CSP process algebra, which provides a precise foundation for software engineering and formal verification using model checking. However, due to state explosion, the application of model checking does not scale. In this paper, we contribute a compositional verification technique that uses Isabelle/HOL RoboChart state machines symbolically. Our technique uses state invariants to capture safety requirements over a very large or infinite state, similar to the B method, and is highly automated using Isabelle's sledgehammer tool. We give a model transformation from the RoboTool development environment to Isabelle/HOL and apply this to several verification case studies.
Original languageEnglish
Title of host publication27th International Conference on Engineering of Complex Computer Systems
PublisherIEEE
Publication statusAccepted/In press - 16 Mar 2023
Eventthe 27th International Conference on Engineering of Complex Computer Systems - Institut National Polytechnique de Toulouse, Toulouse, France
Duration: 14 Jun 202316 Jun 2023
https://www.irit.fr/iceccs2023/

Conference

Conferencethe 27th International Conference on Engineering of Complex Computer Systems
Abbreviated title ICECCS 2023
Country/TerritoryFrance
CityToulouse
Period14/06/2316/06/23
Internet address

Bibliographical note

This is an author-produced version of the published paper. Uploaded in accordance with the publisher’s self-archiving policy. Further copying may not be permitted; contact the publisher for details

Cite this