Research on generation of testing data in hybrid method of model checking and testing

In this paper, hybrid method of model-checking and testing were suggested, the testing process for the combination of model-checking and testing were given. Counterexample of model-checking on LOTOS lacking in testing data which lead to the test suite generating based counterexample lacking in pertinence. In order to guarantee the significance of the testing based on counterexample, it proposes the LOTOS complex data type expansion method and the method for generating the testing data in the process of LOTOS modeling in service. By giving an instance researched of model-checking and testing service to prove the validity of the data generation technology.