Title :
Towards formalizing UML state diagrams in CSP
Author :
Ng, Muan Yong ; Butler, Michael
Author_Institution :
Dept. of Electron. & Comput. Sci., Southampton Univ., UK
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;
Conference_Titel :
Software Engineering and Formal Methods, 2003.Proceedings. First International Conference on
Conference_Location :
Brisbane, Queensland, Australia
Print_ISBN :
0-7695-1949-0
DOI :
10.1109/SEFM.2003.1236215
