DocumentCode :
3459907
Title :
Formalization of UML statechart diagrams in the π-calculus
Author :
Lam, Vitus S W ; Padget, Julian
Author_Institution :
Dept. of Math. Sci., Univ. of Bath, UK
fYear :
2001
fDate :
2001
Firstpage :
213
Lastpage :
223
Abstract :
This paper presents a systematic approach for the translation of UML statechart diagrams into the π-calculus. The aim of this study is to demonstrate how a semi-formal specification can be transformed to a verifiable specification expressed in the π-calculus such that the behaviour of the system can be formally analyzed. The translation covers the major features of statechart diagrams, including internal transitions, triggerless transitions, conflicting transitions, actions, activities, non-concurrent composite states, history pseudostates, concurrent composite states, etc. The desired behavioural properties of statechart diagrams are identified. In addition, the correctness of the translation is proved by showing that the π-calculus expressions satisfy these behavioural properties
Keywords :
formal specification; pi calculus; specification languages; π-calculus; UML statechart diagrams; behavioural properties; semi-formal specification; statechart diagrams; Algebra; Calculus; Carbon capture and storage; Computational modeling; Concurrent computing; LAN interconnection; Object oriented modeling; Safety; Unified modeling language; Visualization;
fLanguage :
English
Publisher :
ieee
Conference_Titel :
Software Engineering Conference, 2001. Proceedings. 2001 Australian
Conference_Location :
Canberra, ACT
ISSN :
1530-0803
Print_ISBN :
0-7695-1254-2
Type :
conf
DOI :
10.1109/ASWEC.2001.948515
Filename :
948515
Link To Document :
بازگشت