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.
|Title of host publication
|27th International Conference on Engineering of Complex Computer Systems
|Accepted/In press - 16 Mar 2023
|the 27th International Conference on Engineering of Complex Computer Systems - Institut National Polytechnique de Toulouse, Toulouse, France
Duration: 14 Jun 2023 → 16 Jun 2023
|the 27th International Conference on Engineering of Complex Computer Systems
|14/06/23 → 16/06/23