A formal execution semantics and rigorous analytical approach for communicating UML statechart diagrams  Posted on:20070901  Degree:Master  Type:Thesis  Country:China  Candidate:Lam, Vitus S. W  Full Text:PDF  GTID:2458390005983323  Subject:Computer Science  Abstract/Summary:  PDF Full Text Request  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 modelchecking 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 channelpassing 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 equivalencechecking 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.  Keywords/Search Tags:  UML, Statechart diagrams, Semantics, Approach, Formal, Using  PDF Full Text Request  Related items 
 
