Formalizing the semantics of UML statecharts with Z

Author

Xuede Than ; Miao, Huaikou ; Liu, Ling

Author_Institution

Sch. of Comput. Eng. & Sci., Shanghai Univ., China

fYear

2004

fDate

14-16 Sept. 2004

Firstpage

1116

Lastpage

1121

Abstract

UML is a semi-formal language, with a precisely defined syntax and static semantics but with an only informally specified dynamic semantics. UML statechart diagrams are a notation for describing behaviours in the framework of UML. UML statechart diagrams differ from classical statecharts, as defined by Haret, for which formalizations and results are available in the literature. This paper provides a method of formalizing syntax and semantics of UML statecharts with Z. The hierarchical and concurrent structure of states is discussed. This semantics helps to determine whether the software design is consistent, unambiguous and complete.

Keywords

Unified Modeling Language; diagrams; formal specification; programming language semantics; UML statechart diagrams; UML statecharts; Z language; concurrent state structure; dynamic semantics; formal semantics; hierarchical state structure; semiformal language; software design; static semantics; syntax; Digital systems; Mathematics; Object oriented modeling; Packaging machines; Process design; Software design; Software systems; Standards development; Unified modeling language; Visualization;

fLanguage

English

Publisher

ieee

Conference_Titel

Computer and Information Technology, 2004. CIT '04. The Fourth International Conference on

Print_ISBN

0-7695-2216-5

Type

conf

DOI

10.1109/CIT.2004.1357344

Filename

1357344