UML Statecharts Compositional Semantics in LOTOS

Author

Mrowka, Rafal ; Szmuc, Tomasz

Author_Institution

Inst. of Automatics, AGH Univ. of Sci. & Technol., Poland

fYear

2008

fDate

1-5 July 2008

Firstpage

459

Lastpage

463

Abstract

This paper gives an overview of LOTOS-based semantics for compositional UML statecharts. The purpose of this work is to develop a description of a UML statechart model using one of the formal description language - LOTOS.Our approach concentrate on two aspects of the statechart model: concurrency and compositionality. We are using a full LOTOS version to define micro-step semantics which allows to implement cross-state boundaries transitions. Based on the translation function we are able to use a formal statechart model to check the equivalence relations and other model checking techniques.

Keywords

Unified Modeling Language; formal specification; formal verification; programming language semantics; LOTOS-based semantics; UML statechart compositional semantics; cross-state boundary transition; formal LOTOS specification; formal description language; formal statechart model; micro step semantics; model checking technique; translation function; Automata; Broadcasting; Communication standards; Concurrent computing; Distributed computing; Real time systems; Software engineering; Unified modeling language; LOTOS; ROPES; UML statecharts; bisimulation;

fLanguage

English

Publisher

ieee

Conference_Titel

Parallel and Distributed Computing, 2008. ISPDC '08. International Symposium on

Conference_Location

Krakow

Print_ISBN

978-0-7695-3472-5

Type

conf

DOI

10.1109/ISPDC.2008.60

Filename

4724282