DocumentCode :
3176865
Title :
An Operational Semantics for UML RT-Statechart in Model Checking Context
Author :
Zhang, Tao ; Huang, Shaobin ; Huang, Hongtao
Author_Institution :
Coll. of Comput. Sci. & Technol., Harbin Eng. Univ., Harbin, China
fYear :
2009
fDate :
21-22 Dec. 2009
Firstpage :
12
Lastpage :
18
Abstract :
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.
Keywords :
Unified Modeling Language; formal verification; UML RT-Statechart; model checking context; real-time operational semantics; statechart lacking; transition system; Automata; Computer science; Concurrent computing; Context modeling; Educational institutions; Formal verification; Internet; Real time systems; Time factors; Unified modeling language; modelchecking; operational semantics; real time; statechart; transition system;
fLanguage :
English
Publisher :
ieee
Conference_Titel :
Internet Computing for Science and Engineering (ICICSE), 2009 Fourth International Conference on
Conference_Location :
Harbin
Print_ISBN :
978-1-4244-6754-9
Type :
conf
DOI :
10.1109/ICICSE.2009.15
Filename :
5521641
Link To Document :
بازگشت