Institution-based Encoding and Verification of Simple UML State Machines in CASL/SPASS
This work addresses a foundational issue in formal verification for systems engineering, offering a novel alternative to model checking for state-machine analysis.
The paper tackles the problem of analyzing UML state-machines, which are central to model-based systems-engineering, by providing the first correct semantical representation within an institutional framework and enabling symbolic reasoning to handle large or infinite state spaces, overcoming limitations of model checking like state-space explosion.
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.