Software Testing And Reliability Computing Based On Model Rebuilding

With the development of computer software, the scale and complexity problem is becoming more larger, which leads to high expectation on the reliability of the software. Software testing is aimed at detecting and correcting the flaws of the software, is an important tool to ensure and improve the product quality and plays an important role during the development. The key to product testing is test case generating. Reliability is a natural property and an important indicator to quality evaluating. Generating test case and computing reliability are major issues in the study.In this paper, test cases are generated by model checking. The Petri net model of the source program is first built from source code. According to the model, by defining the transformation rules, the Petri net model is transformed into Promela form, which is the input language to model checking tool SPIN. Liner temporal logic (LTL) is used to properties of the program. Counter-examples will be generated by SPIN, which are the test case. By checking all the properties, we will get all the test case.Regarding reliability computing, Nelson model is employed in this paper. By analyzing the test result, we compute the reliability.Finally, an ATM and Bank system example is used to illustrate the benefit of our approach.