  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.
