Research On Model Checking Guides The Generation Of TTCN-3Test Suite

With the development of computer technology, expanding areas of application, size and complexity of software is constantly increasing. In order to guarantee the software quality, software testing technology has become main means of technology.But it is well known that it can only be detected errors as much as possible. so we have to admit using traditional methods to troubleshoot software errors in the system have become increasingly difficult to meet the actual demand.In recent years, model checking because of its high degree of automation, gets the widespread concern of the field of software testing. Model checking’s basic idea is used by the state-space search method to detect a given computational model whether meets the property which the specific modal/temporal logic formulas expressed. Software testing is the traditional means to ensure product reliability and the correctness. Which make it is different from the model checking is the traditional tests use the selected input data set to operate the under test system, and compare the generated output value with the expected value, to determine whether the system is wrong. Due to the limited range of selected test cases, so the traditional testing is notcomplete. On the contrary, model checking is not using a certain set of inputs, but focuses on certain properties to detect whether the system is in line with the statute. However, model checking has its bottleneck. It is the range too broad caused the problem of the state space explosion. Model checking is used in a full space traversal methods to carry out, so in most cases, we need to let model checking and various abstract and generalize principles combine to verify the need of systems.So, for the model checking space explosion and the incompleteness of software testing, in the testing process, put the model checking before the customary testing, combine model checking and testing. Through analysis of the formal specification of model checking to clear testing purposes, then brings it into TTCN-3abstract test suite. Further, using the example exists in the formal specification, associated it with a data type description file, to set up test cases. Analyze the TTCN-3development model, based on the equivalence of a labeled transition system and TTCN-3behavior trees, this paper put forward a guide of hypothetical model test suite generation algorithm, and implements the automatic generation of TTCN-3abstract test suite.