EFSM Model Based Optimal Generation And Instantiation Of Test Cases

With the rapid development of information technology, the software product isapplied to all areas of society. Quality of software products naturally become thefocus of common concern. Software testing plays an increasingly role throughout thesoftware development process. But now the cost of traditional manual testing isexpensive, it urgently needs to automate the testing process. Model-based testingmakes testing automatically possible, which will greatly reduce the cost of softwaretesting.Model-based tesing is an effective method of software tesing. It uses behavioralmodel to specify the desired output of system under test and the possible behavior ofenvironment. The input-output pair of the model is regard as the test cases of theactual system. The output of the model is the desired output of the system under test.Applying the model checking to model-based testing to automatically generate testcases has become a research hotspot.This thesis has four contributions:First, the test suite generated using model-based testing usually containsredundancy, which greatly increase the cost of tesing execution. In order to reducethe test suites during the generation of the test cases, a test suite reduction methodbased on satisfiabiliy is proposed. EFSM is as modeling tool used to specify thesystem model, and the LTL is used to specify the test target. Test goal to generate testcase is selected according to the hardness of the corresponding CNF. For theselectede test goal, test case (counterexample) is generated using model checking. Inorder to reduce the test suite, we decide whether the generated test case covers thethe rest test goals using satisfiability to reduce the test suites.Second, we use counterexample guided abstraction refinement to reduce the testsuites further based on above method we proposed. The equivalence class of thestates in the EFSM is defined according to formual cluster, the correspondingtransitions can be merged in different situations, after this, an abstract EFSM modelcan be built, and the counterexamples are generated from the abstraction modelusing model checking. The method deciding whether a counterexample is a spuriouscounterexample is proposed. If it is a spurious counterexample, an abstractionrefinement framework is used to refine the abstraction model. Finally, we get theoptimized test suite using the test case generation method based on satisfiability weproposed before.Third, the test cases generated by model checking are just states sequence,while the complete test cases should include test data and desired output. In order toexecute the test cases generated by model checking, it is necessary to instantiatethem. A method to generate test data for the paths in EFSM model is proposed. Kalaji’s approach uses genetic algorithm to generate test data. We analyze thedeficiencies of Kalaji’s approach, and improve it. An algorithm consideringcondition coverage ratio is proposed. When calculate the fitness of the individual, weconsider the brach distance and the ratio of uncovered conditions at the same time.Fourth, many transition paths generated by random method are infeasible, andgenerate test data for these paths are time-wasting. We consider the feasibility of thepaths in EFSM model. The related transition set of the specified transition can be getusing slicing. And the feasibility of the paths is decided by theorem proving.Moreover, we conducted detailed evaluation to validate the proposedapproaches.Lastly, a component based system-Generic Patient Controlled Analgesia PumpModel is used to explain the method proposed in this paper. First this system isintroduced briefly and the EFSM model of each component in the alarm detectionstate machine is given. The abstraction model of each component is generated usingcounterexample guided abstraction refinement, and the abtraction model of theparallel component is obstained by parallel combing each component. The test suiteof this model is generated by the satisfiability based method. And the test data ofeach test case is generated by the method we proposed.