We present a new approach on how to provide institution-based semantics for UML state machines. Rather than capturing UML state machines directly as an institution, we build up a new logical framework M_D~↓ into which UML state machines can be embedded. A theo-roidal comorphism maps M_D~↓ into the CASL institution. This allows for symbolic reasoning on UML state machines. By utilising the heterogeneous toolset HETS that supports CASL, a broad range of verification tools, including the automatic theorem prover Spass, can be combined in the analysis of a single state machine.
展开▼
