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, and considers a subset of UML that in the author's opinion is expressive enough for protocol models but allows a simpler translation to SPIN than existing work.