A formal execution semantics and rigorous analytical approach for communicating UML statechart diagrams

The major problem of the official UML semantics is it lacks the precise definition which is required for performing a formal analysis and reasoning on statechart diagrams. This thesis first examines a rigorous approach for the formalization of the execution semantics of communicating UML statechart diagrams in the π-calculus. An integrated approach which is based on the formalized execution semantics is then proposed for the equivalence checking and model checking of statechart diagrams.;Likewise, we put forward a model-checking environment. To verify the correctness of a finite state system represented as multiple interacting statechart diagrams, we specify the design in statechart, diagrams using Poseidon for UML, formalize them in the π-calculus, transform the π-calculus expressions into equivalent NuSMV code using PiCal2NuSMV and verify the system automatically using the NuSMV model checker.;Our work illustrates how an integrated approach can provide a more thorough analysis of statechart diagrams. The main contributions of this thesis are: (i) a formal definition of the execution semantics of statechart diagrams; (ii) an integration of different formal methods and tools for analyzing statechart diagrams, and (iii) a practical application of the proposed approach for verifying the correctness of SET/A protocol.;Our formalization transforms a subset of UML statechart diagrams as distinct from statecharts into the π-calculus as a number of processes which communicate via a channel-passing interaction paradigm. Checking equivalence of any two statechart diagrams is transformed to a problem of verifying whether the corresponding π-calculus process expressions are equivalent. An equivalence-checking environment which consists of three software tools is described and demonstrated. The environment allows a user to draw statechart diagrams with Poseidon for UML, translate them into π-calculus representations with SC2PiCal and check whether the statechart diagrams are equivalent using the MWB.