USMC: A Self-contained Tool for Model Checking UML State Machine Diagrams

Model based design is widely adopted in modern software development procedure. UML diagrams have become the de-facto modeling language in object oriented system designs. UML state machine diagrams are specifically used in modeling dynamic behaviors of a class. It has been widely agreed that verification of system designs at an early stage will dramatically reduce the development cost. A large number of work has been done on formalizing UML state machine semantics, some of them have been implemented in tools. These tools are usually model translators which provide a front-end implementation of the translating rules to a back-end model checker. However, state-of-the-art does not necessarily turn into state-of-the-practice since we see few report of usage of those tools. In this work, we report a tool which aims at turning model checking of UML state machine dynamic behaviors into practice. Our tool named USMC provides user-friendly interfaces for simulating UML state machines as well as powerful model checking support for LTL and deadlock-freeness properties.

Our implementation is based on the formal operational semantics we had defined for the full set of UML state machine diagrams. The detailed semantics is available in our technical report.[pdf]

The vedio below demonstrates the utilities of our tool.

Please contact Liu Shuang liushuang@comp.nus.edu.sg if you have any questions, or want to contribute to our USMC tool