An Interface Language Between Specification and Testing
Citation
- G. Fink, M. Helmke, M. Bishop, and K. Levitt, “An Interface Language Between Specification and Testing”, Technical Report CSE-95-15, Dept. of Computer Science, University of California at Davis, Davis, CA 95616-8562 (Aug. 1995).
Paper
About This Report
From the introduction:Specifications describe models that programs are supposed to implement. Testing is used to verify if a program’s implementation is correct. Specification languages such as Z don’t provide ways to relate this model to a program state. Alternatively, the program couuld be developed independent of the specification, so there is no natural correspondence between specification and code.
In this paper, we present a new specification language TASPEC which can serve as an intermediary between a Z specification and the testing process. TASPEC can express close correspondences between code and abstract semantics. Large portions of Z are shown to be semi-automatically translatable into TASPEC. Test oracles and other testing artifacts can be derived from TASPEC specifications. As an example, a recently discovered flaw in an implementation of the TCP protocol is uncovered using this technique.
