Formalization of UML Statechart Diagrams in the π-calculus

This paper presents a systematic approach for the translation of UML statechart diagrams into the /spl pi/-calculus. The aim of this study is to demonstrate how a semi-formal specification can be transformed to a verifiable specification expressed in the /spl pi/-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 /spl pi/-calculus expressions satisfy these behavioural properties.