Formalize the Time-extended UML Statechart with Timed Automata
Lai Ming · Jisuanji gongcheng · 2003
Rigorous Modeling is a core technology in embedded realtime system design and the combination of UML and formal methods would provide a better tool support to it. In this paper, an approach is given to transform timeextended UML statechart into timed automata, which is a formal model. A timeextended UML statechart is suitable to model a dynamic view of embedded realtime system, and timed automata is easier to be expressed in formal specification. Our approach bridges the gap of UML and formal methods.