Institution-based Encoding and Verification of Simple UML State Machines in CASL/SPASS

TL;DR

This paper introduces a correct semantic encoding of UML state-machines within an institution framework, enabling symbolic analysis via theorem-provers to address large or infinite state spaces.

Contribution

It provides the first accurate semantical representation of UML state-machines in an institution, facilitating symbolic reasoning beyond traditional model checking.

Findings

First correct semantic encoding of UML state-machines in an institution

Enables symbolic analysis using theorem-provers

Addresses state-space explosion problem in state-machine analysis

Abstract

This paper provides the first correct semantical representation of UML state-machines within the logical framework of an institution (previous attempts were flawed). A novel encoding of this representation into first-order logic enables symbolic analyses through a multitude of theorem-provers. UML state-machines are central to model-based systems-engineering. Till now, state-machine analysis has been mostly restricted to model checking, which for state-machines suffers heavily from the state-space explosion problem. Symbolic reasoning, as enabled and demonstrated here, provides a powerful alternative, which can deal with large or even infinite state spaces. Full proofs are given.