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

Tobias Rosenberger, Saddek Bensalem, Alexander Knapp +1

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 encodi…