An Automatic Approach to Model Checking UML State Machines

UML has become the dominant modeling language in software engineering arena. In order to reduce cost induced by design issues, it is crucial to detect model-level errors in the initial phase of software development. In this paper, we focus on the formal verification of dynamic behavior of UML diagrams. We present an approach to automatically verifying models composed of UML state machines. Our approach is to translate UML models to the input language of our home grown model checker PAT in such a way as to be transparent for users. Compared to previous efforts, our approach supports a more complete subset of state machine including fork, join, history and submachine features. It alleviates the state explosion problem by limiting the use of auxiliary variables. Additionally, this approach allows to check safety/liveness properties (with various fairness assumptions), trace refinement relationships and so on with the help of PAT.