The Design And Implementation Of Software Testing Tool Based On Z Specification

The testing task of modern software is becoming more and more difficult due to the huge scale of software and the quickly development of computer industry. Extra attention has been paid to how to improve the test job. The formal specification has a history of about 30 years. The advantage of it is the mathematic base and specific description. It will largely reduce the mistake in the coding and testing process if we introduce formal specification to the lifecycle of software. Based on formal specification, this paper proposes a new method to detect weaknesses and vulnerabilities in the software which focus on the testing period of the life circle of software.According to the existing software testing method and black-box test, a formal software test method is proposed. Firstly, we should get the Z specification of the object system and do a general analyst to it. Secondly, generate test cases from the results which is given by step 1 and simplify these test cases. Finally, obtain the object project codes and run them with test cases. Then compare the results of codes with the output of test cases to determine if weakness exists.Furthermore, this paper designs and implements a security testing tool whose functional modules including Z specification analyst, an automated test case generating module and a test-executing module. The tool is implemented by plug-in techniques of Eclipse development platform and can be further integrated into other secure software development environment.The testing tool provides testers with comparative automated tool supports, and reduces the dependency of security tests on testers'skills and experiences, and enhances the developing speed. The integration of this tool into a secure software development environment exerts a positive effect on building secure and reliable software.