Object-oriented Formal Specification Based Test Generation

With the development of information technique, the software grows larger and larger. How to guarantee and improve the software quality becomes the main concerned point in the field. As one of the key techniques of guaranteeing software quality, software testing can effectively detect the faults in the system. According to the statistics, the cost of software testing accounts for 40% in the whole cost of software development. With the enlarging of software, the proportion of software testing grows larger in the software development. For some safety critical system, the cost of testing almost corresponds to the triple or quintuple cost of all other developing phase. Thus, improving the effectivity and efficiency of testing and reducing the software developing cost becomes one of the urgent tasks for software engineers.The core problem of software testing is test cases generation. According to the source that is used to derive tests, software testing is classified into two categories -program based testing and specification based testing. Program based testing means testers use program structures to derive test cases. Specification based testing means testers use the specification instead of program structures to derive test cases. The specification based testing can verify whether a program conforms to its specification, which is the aim of testing. Furthermore, during specification based testing process, the development of test cases can be parallel with the software development. That can reduce the time of software development, and improve development efficiency.Since formal specifications possess precise notations and clear semantics, and can be used in reasoning and proving, taking formal specifications as the source of generating test cases makes automatic test cases generation possible. However, most research of formal specification based test generation focuses on applying black-box test criteria (such as category partition criteria, state graph based criteria) on different forms of formal specifications (such as, Z schema, UML state chart) to generate test cases. For model-based object-oriented formal specifications (such as, Object-Z, VDM++ specifications), those methods are very hard to be applied. The main causes are that there is no state chart notation in the specifications and it is hard to apply category partition criteria to those complicated predicates in the specifications.This paper provides a series of techniques that is used to derive test cases from model-based object-oriented formal specifications. Those techniques discuss the problems of deriving test cases at class level and intra-class level respectively. At class testing level, this paper defines a set of axioms that is used to evaluate the existing logic coverage criteria, which are applied in the intra-method testing. The evaluation provides testers with a guide of selecting logic coverage criterion. Moreover, at the class testing level, this paper also presents a set of intra-class testcriteria, which is used to generate intra-class test cases from infra-method tests. Those intra-class test cases can test the interactions among the public methods of a class. Those criteria avoid the extra burden of extracting class state graph from class specification and make mechanical generating infra-class test cases possible. At inter-class testing level, this paper presents a series of test criteria that are used to test the polymorphism relation in a class hierarchy. These inter-class criteria are different from program based polymorphism test criteria. They are used to derive test cases from formal specification. These test cases can check whether the polymorphism relationship implemented in a program conforms to that defined in the specification.Besides above test criteria, this paper also gives a testing framework to describe the test case generation process. This testing framework is defined with Object-Z notation, which is adopted in the specifications. It reduces the understanding burden for readers while adopting another notation.