Model Checking of UML State Machines
Wei Yu Dong · Computer Engineering and Science · 2001
Model checking is a very important method of automatic formal verification to ensure the correctness of design specifications.We give a method for the model checking of UML state machines in this paper.First,we describe the syntax and semantics of UML state machines.Based on the RTC step in the semantics,we give a method to construct the global transition graph of reachable states.The core of the method is to determine all maximal non conflict transition sets.Finally,we give algorithms to verify if the UML state machine satisfies the properties described in compute tree logic(CTL).