Testing And Verification Methods Based On UML2.0Models

Unified Modeling Language (UML) is a visual modeling language with powerful description ability and intuitionistic meaning. It provides various diagrams to depict system characteristics and complex behaviors from different viewpoints and application layers. UML-based software developing process and modeling environments have been widely accepted in the academic and industrial, but the lack of precise semantics for graphical symbols makes it difficult to verify the correctness of UML and judge if the models satisfy the requirements. So the formal specification and verification of UML models has become a key issue.This dissertation mainly focuses on the UML2.0models, in which a specification method based on event deterministic finite automata (ETDFA) and a verification method based on propositional projection temporal logic (PPTL) for sequence diagrams (SD) are proposed. On the basis of verified automata, synthesis rules are used to get the composed automata, and an incremental test case generation algorithm is applied to obtain the set of test cases. To ensure the correctness of interactive behaviors in distributed software systems, the modeling, verification and testing methods of interactive actions are discussed. System state machine diagrams, object state machine diagrams and sequence diagrams are introduced to model the state transitions and interactive behaviors in modules respectively. Verification and testing methods can confirm the correctness of models and their interactive behaviors.The main contributions of the dissertation are as follows:(1) A formal description method for UML2.0sequence diagrams is presented. With the grammar and semantic of SD, the7-tuple definition of ETDFA and the algorithm of constructing ETDFA based on SD, a formal description process can be accomplished.(2) To analysis and verify the automata models of SD, PPTL model checking is adopted in this thesis. The verification results can be obtained by an algorithm of model checking ETDFA with PPTL formulas being the properties. Finally, with the implementation of a PPTL model checker based on Spin, the ETDFA models of SD are verified.(3) The key techniques of test cases generation from models are analyzed and an incremental test case generation method is proposed. Event deterministic finite automata are employed to describe the sequence diagrams models of software systems. Further, a synthesis algorithm is given to get the composed automata. In addition, to generate the test cases incrementally, the test scenarios generation rules and test cases generation algorithm are presented in this thesis. This approach improves test cases correctness, and reduces the complexity of test cases generation process. (4) To ensure the correctness of interactive behaviors among the modules in distributed software systems, a modeling method which uses system state machine diagrams, object state machine diagrams and sequence diagrams to describe the state transitions and interactive behaviors in modules is proposed in this dissertation. PPTL model checking is adopted to verify whether the interactive modules can satisfy the system properties. On the basis of verified sequence diagrams, test case generation method is used to get the set of test cases to test the interactive behaviors.(5) A tool called SDTA is devised and built, which supports a full transformation from SD to ETDFA automatically. With the tool, UML models and automata can be directly created. Then the source models are translated with rules into target models by SDTA.