M. Ng, and M. Butler. Software Engineering and Formal Methods, 2003.Proceedings. First International Conference on, page 138 -- 147. (September 2003)
DOI: 10.1109/SEFM.2003.1236215
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.
%0 Conference Paper
%1 ng_towards_2003
%A Ng, Muan Yong
%A Butler, M.
%B Software Engineering and Formal Methods, 2003.Proceedings. First International Conference on
%D 2003
%K , Model, analysis; and, behaviour, checker; communicating, decision, diagrams; formal, formalisation; language, language; languages; modelling, processes; programming, semantics; sequential, specification, specification; state, structural, systems, unified, verification {UML},
%P 138 -- 147
%R 10.1109/SEFM.2003.1236215
%T Towards formalizing UML state diagrams in CSP
%X 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.
@inproceedings{ng_towards_2003,
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.}},
added-at = {2013-02-28T11:13:35.000+0100},
author = {Ng, Muan Yong and Butler, M.},
biburl = {https://www.bibsonomy.org/bibtex/26f66224a26d2f05702c59768129febc0/fritzsolms},
booktitle = {{Software Engineering and Formal Methods, {2003.Proceedings.} First International Conference on}},
doi = {10.1109/SEFM.2003.1236215},
interhash = {fcf4908468fda03cf4cedc7885c4bb4e},
intrahash = {6f66224a26d2f05702c59768129febc0},
keywords = {, Model, analysis; and, behaviour, checker; communicating, decision, diagrams; formal, formalisation; language, language; languages; modelling, processes; programming, semantics; sequential, specification, specification; state, structural, systems, unified, verification {UML},},
lccn = {0036},
month = sep,
pages = {138 -- 147},
timestamp = {2013-02-28T11:14:00.000+0100},
title = {{Towards formalizing {UML} state diagrams in {CSP}}},
year = 2003
}