Equivalence checking of communicating UML statechart diagrams

V. S. W. Lam, J. Padget

Research output: Contribution to journalArticlepeer-review


We demonstrate how a subset of UML statechart diagrams (SCDs) as distinct from statecharts is encoded in the π-calculus as a number of processes which communicate via a channel-passing interaction paradigm. An extension to the original UML semantics for communicating statechart diagrams is presented. Different sorts of equivalences of UML SCDs encompassing isomorphism, strong behavioural equivalence and weak behavioural equivalence are defined. Determining equivalence of any two UML SCDs is transformed to a problem of checking whether their respective π-calculus process expressions are equivalent. The practicality of the approach is exemplified using an industry level case study.
Original languageUndefined/Unknown
Pages (from-to)265-304
Number of pages40
JournalInternational Journal of Software Engineering and Knowledge Engineering
Issue number2
Publication statusPublished - 2012

Cite this