Automating Verification of State Machines with Reactive Designs and Isabelle/UTP

TL;DR

This paper introduces an automated, scalable verification method for state machines in robotic systems using theorem proving and UTP semantics, demonstrated through deadlock-freedom checks in Isabelle/UTP.

Contribution

It develops a formal, mechanised verification framework for state machines with infinite states, integrating UTP semantics and theorem proving in Isabelle/UTP.

Findings

Automated deadlock-freedom verification for infinite state systems.

Mechanisation of state machine semantics in Isabelle/UTP.

Demonstration of practical verification tool using UTP.

Abstract

State-machine based notations are ubiquitous in the description of component systems, particularly in the robotic domain. To ensure these systems are safe and predictable, formal verification techniques are important, and can be cost-effective if they are both automated and scalable. In this paper, we present a verification approach for a diagrammatic state machine language that utilises theorem proving and a denotational semantics based on Unifying Theories of Programming (UTP). We provide the necessary theory to underpin state machines (including induction theorems for iterative processes), mechanise an action language for states and transitions, and use these to formalise the semantics. We then describe the verification approach, which supports infinite state systems, and exemplify it with a fully automated deadlock-freedom check. The work has been mechanised in our proof tool, Isabelle/UTP, and so also illustrates the use of UTP to build practical verification tools.