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

Volume

1

fYear

2009

fDate

21-22 Nov. 2009

Firstpage

381

Lastpage

385

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;

fLanguage

English

Publisher

ieee

Conference_Titel

Intelligent Information Technology Application, 2009. IITA 2009. Third International Symposium on

Conference_Location

Nanchang

Print_ISBN

978-0-7695-3859-4

Type

conf

DOI

10.1109/IITA.2009.309

Filename

5369629