Research On Automatic Generation Of Test Cases Based On Multi-value Model Detection

With the development of computer technology, people's life increasingly depend on the assistance of computer, such as mobite computing, communication systems, information management systems, intelligent medical system, smart house and so on. All of these need support of software. A common question is how to solve a variety of problems to ensure the quality of software.Software testing is an effective method for ensuring software quality and reliability. The procedure of software testing consumes a large-scale manpower, materials and time, which use 40% to 60% resource of total software development. Therefore, software test automation is very important for ensuring software quality and reducing the cost of software development. What's more, test case auto-generation is the key component for software test automation.Model checking has caught more and more attention, because it has the advantage to help to generate test cases automatically. The existing research on test case auto-generation is generally based on classical logical model checking, which mainly use the explicit state search or implicit fix-point computation to verify the modal/proposition properties of finite state concurrent system and provide counterexamples when the system doesn't satisfy the properties. Finally, test cases can be extracted from counterexamples. However, the scale and complexity of system increasing leads to obtaining model more difficult. Furthermore, it is easy to bring state explosion when the system states are exhaustive searched by classical logical model checking. All of these questions should be solved to realize the test cases auto-generation. Therefore, some new methods should be introduced to generate test case automatically. Fortunately, multi-valued model checking provides a practicable basis to solve the above problem. This paper presents a method of test case auto-generation based on multi-valued model checking. The main contributions of this paper are as follows:Firstly, this paper analyzes the status and issues of test case auto-generation based on model checking.Secondly, this paper describes the theoretical basis of multi-valued model checking.Thirdly, this paper presents a method of test case auto-generation based on m multi-valued model checking. This method uses temporal logic formulas to describe the system properties, the variation of temporal logic formulas by the trap properties to satisfy the test coverage, proposes a verification to verify the variation of CTL and generate counterexamples.Finally, this paper illustrates the steps to extract test sets from the counterexamples.In conclusion, this method based on multi-valued model checking we proposed can be used to automatically achieve the test cases of complex system, which provides a good base for complex system testing in realistic industry environment.