An Operational Semantics for UML State Machines in Model Checking Context
Xuandong Li · Dianzi xuebao · 2003
The state machine formalism in UML is used for modeling discrete behavior of various system elements.Its rich notation provides a powerful description mechanism which meanwhile decreases modality of its structure and increases verifying complexity.Model checking is a technique for automatically verifying finite-state concurrent systems.By model checking the behavior of various system elements described by SM,we can find design errors as soon as possible.This paper defines an operational semantics for SM using Kripke structure in order to model checking SM.Different from existing SM semantics definitions,this paper takes undetermined factors in SM into consideration .SM is translated into kripke structure that describes all possible evolving traces on which model checker checks.