Research On A Method Of Test Cases Generation Based On Timed Automata

Software testing is the most fundamental and important way to improve software reliability and guarantee the correctness of software. And the design of test cases is the key issue of software testing. It is also a fundamental guarantee of the quality of software testing. With the increasing scale of software systems and the expanding of applications, the testing of software systems becomes more difficult. Therefore, the techniques of automated software testing have become an important research directions in recent years.Model based test cases generation has been developed as a prominent technique in testing of reactive software systems. It uses formal methods to model the system and generates test cases based on the model. Model checking is one of the main technologies that are used in model based test case generation. So it is inevitable to meet the state-space explosion problem in the process of deriving test cases. In addition, temporal logic errors in the systems would perhaps lead to disastrous consequences for real-time systems. Therefore, how to avoid the state-space explosion in the test case generation and try to find implied temporal errors of software are the main questions discussed in this thesis.The thesis studies the method of test case generation based on timed automata and analyzes a class of real-time system with different time scales. A technique of improvement on a method of test cases generation based on timed automata is proposed. The original structure of timed automata model is improved to reduce the impact of the state-space explosion. Accordingly the velocity of model-based test cases generation is enhanced and the size of the generated test suite is reduced.Real-time systems are often concurrent, so the response time depends on the execution time and order of different tasks. After studying on a method of mutation testing based on timed automata extended with tasks and analyzing deeply the characteristics of internal behaviors of concurrent real-time system and all possible ways of test hypothesis, this thesis gives a new way of mutation testing. We define a few kinds of mutation operator for simulating a variety of timing errors of real-time systems. We use the tool of scheduling analysis TIMES to model the real-time systems. And the timed automata model of system is mutated by our mutation operators. This method can generate test sequences which can reveal timing errors of systems.