An Integrated Environment for Communicating UML Statechart Diagrams

Existing UML modelling tools provide only a limited support for the analysis of UML statechart diagrams. This paper describes the implementation and integration of an environment for analyzing UML statechart diagrams in two different ways. These include equivalence checking and model checking. To prove the equivalence of two statechart diagrams, we draw the two diagrams using Poseidon for UML, translate them into the pi-calculus using the SC2PiCal and check whether they are equivalent or not using the MWB. To verify the correctness of a system represented as multiple communicating statechart diagrams, we draw the diagrams using Poseidon for UML, translate them into the pi-calculus using the SC2PiCal, transform the pi-calculus expressions into equivalent NuSMV code using the PiCal2NuSMV and check the validity of the system using the NuSMV model checker.