Model Checking Dynamic and Hierarchical UML State Machines

This paper presents a technique to model check UML specifications by translating UML models to the model checker SPIN. Our models consist of active UML classes, whose behavior is defined by hierarchical state machines. The intended application is to find errors in protocols communicating using asynchronous message passing. Compared to previous efforts using a similar approach, our novel points are the following. First, we consider a subset of UML that in our opinion is expressive enough for protocol models but allows a simpler translation to SPIN than existing work. Preliminary analysis of simple industrial models support our conclusions on the expressivity of our UML subset. Second, we present a powerful action language that is still amenable to automatic analysis. The action language is used to specify the effects of transitions, which may include dynamic creation of new objects. Finally, we discuss an even simpler SPIN translation for flattened UML state machines and compare it to the translation that supports hierarchy.