An Interface Language Between Specification and Testing



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.


This is part of the property-based testing project. It shows how to map formal specifications into testing specifications for two specific languages.