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
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;
Conference_Titel :
Software Engineering Conference, 2001. Proceedings. 2001 Australian
Conference_Location :
Canberra, ACT
Print_ISBN :
0-7695-1254-2
DOI :
10.1109/ASWEC.2001.948515