An Operational Semantics for UML RT-Statechart in Model Checking Context

Model checking UML statechart can detect various errors and inconsistencies of current system design in the early process of development. However, because of classic statechart lacking of real-time operational semantics, it can not be directly used to verify real-time property of current system. This paper introduces related definition of clock to extend UML statechart to real-time UML statechart, defines the main elements of statechart by tuple and proposes a middle expression form of statechart SC. Through defining the operational semantics of SC, the conversion from SC to transition system is achieved and a conversion algorithm is given. Based on the above theories, the general approach for model checking SC is described, and in the end, a classic study case of conversion from SC to TS is given.