UML Consistency Checking And Test Case Generation Based On Model Checking

Along with the application of computer software development, people propose higherrequirement of software quality and reliability. System modeling and software testing are usually usedto ensure them. Model checking, as a formal verification technique, has many advantages, such asautomation and providing counterexamples and so on. So this paper mainly studies the modelchecking used in checking the UML consistency and the automatic generation of test cases, so as toensure the software high reliability.UML is a visualized graphical modeling language with powerful ability and intuitionisticmeaning. However, there is existing a certain amount of information redundancy andcross-interleaving among models corresponding to each aspect of the resulted representation system,some unconsistency problems will possibly appear between UML models. This paper puts forward aconversion rule from sequence diagram and state diagram in UML2.0to SMV language, solving thesequence diagram characteristics of combination fragments and asynchronous message. The statediagram and sequence diagram are expressed as SMV language model and CTL temporal logic, andthen using model checking tool NuSMV checks the consistency. Finally, based on the above reaserchwork, this paper designs and develops a UML checking consistency tool.Software testing is a critical step to ensure software quality, and its core issue is the automatictest case generation. After researching a method of automatic generation of test cases based on modelchecking, this paper puts forward a fast generation algorithm based on binary tree to construct thetemporal logic. Combined with a test process of automatically generating test cases which is based onsoftware requirement and takes use of model checking, generate test cases to meet MC/DC coveragecriterion. Finally, this paper designs and realizes an automatic generation tool of test cases based onthe model checking. Combined with the avionics system, uses the existing tools, TestBed, to verifythe test cases validity and the coverage of test cases.