Towards formalizing UML state diagrams in CSP

Author

Ng, Muan Yong ; Butler, Michael

Author_Institution

Dept. of Electron. & Comput. Sci., Southampton Univ., UK

fYear

2003

fDate

22-27 Sept. 2003

Firstpage

138

Lastpage

147

Abstract

The UML (Unified Modeling Language) state diagram notation by M. Fowler and K. Scott (2000) is a graphical language which comprises an extensive set of constructs with good structural semantics but lack of a formal behavioral semantics. With this regard, we have used the Hoare´s CSP (Communicating and Sequential Processes) to formalize the behavior of UML SD. The fact that CSP is supported by model-checkers such as FDR enables a system design using a state diagram to be formally checked during design stage. This paper presents the formalization which would allow us to reason about the behavior of UML SD in CSP.

Keywords

communicating sequential processes; decision diagrams; formal specification; formal verification; programming language semantics; specification languages; systems analysis; UML state diagrams; behaviour formalisation; communicating and sequential processes; model checker; structural semantics; unified modelling language; Computer science; Logic; Prototypes; Software engineering; Unified modeling language;

fLanguage

English

Publisher

ieee

Conference_Titel

Software Engineering and Formal Methods, 2003.Proceedings. First International Conference on

Conference_Location

Brisbane, Queensland, Australia

Print_ISBN

0-7695-1949-0

Type

conf

DOI

10.1109/SEFM.2003.1236215

Filename

1236215