Title :
UML Statecharts´ PTL Formal Semantics
Author :
Zhang, Pengfei ; Zhenhua Duan ; Tian, Cong
Author_Institution :
Sch. of Comput. Sci. & Technol., Huaibei Coal Ind. Teachers´´ Coll., Huaibei, China
Abstract :
An approach for transforming UML statecharts into Projection Temporal Logic(PTL) formal models for system´s simulation and verification is presented in this paper. UML Statechart is a graphic tool used to describe systems´ behaviors, but it lacks formal semantics. PTL is a kind of temporal logic interpreted over discrete state sequences (intervals). With PTL, the formal semantics of UML Statecharts is defined. By transforming a UML statecharts into PTL model and describing properties with PTL, the system can be formally verified in the same logic frame and further simulated by Tempura-an executable subset of PTL. A tool has been developed for automatically transforming UML statechart diagrams into PTL formal models which will facilitate system´s simulation and verification.
Keywords :
Unified Modeling Language; formal verification; temporal logic; Tempura; UML statechart diagrams; Unified Modeling Language; discrete state sequences; formal model; formal semantics; graphic tool; projection temporal logic; system simulation; system verification; Application software; Computer science; Educational institutions; Embedded system; Fuel processing industries; Graphics; Information technology; Logic testing; Process design; Unified modeling language; Formal Semantics; Projection Temporal Logic; Simulation; UML Statecharts; Verification;
Conference_Titel :
Intelligent Information Technology Application, 2009. IITA 2009. Third International Symposium on
Conference_Location :
Nanchang
Print_ISBN :
978-0-7695-3859-4
DOI :
10.1109/IITA.2009.309
