A formal execution semantics and rigorous analytical approach for communicating uml statechart diagrams
Vitus S. W. Lam · The University of Bath Online Publications Store (The University of Bath) · 2006
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.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.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 Abstract (iii) a practical application of the proposed approach for verifying the correctness of SET/A protocol.