Specification-based testing is important because it relates directly to what the program is supposed to do and can detect certain errors that are often not detected by traditional code-based testing techniques such as branch coverage and statement coverage. We have developed an automated testing tool, called ADLscope, that utilizes the formal specification of a program unit as the basis for test coverage measurement. A tester uses ADLscope to test application programming interfaces (APIs) written in the C programming language. The API must be formally specified in the Assertion Definition Language (ADL). The tester uses ADLscope to generate coverage conditions from a program's ADL specifications. When the API is tested, ADLscope automatically measures how many of the coverage conditions have been covered by the tests.

This paper describes a specification-based black-box technique for testing program units. The main contribution is the method that we have developed to derive test conditions, which are descriptions of test cases, from the formal specification of each program unit. The derived test conditions are used to guide test selection and to measure comprehensiveness of existing test suites. Our technique complements traditional code-based techniques such as statement coverage and branch coverage. It allows the tester to quickly develop a black-box test suite.In particular, this paper presents techniques for deriving test conditions from specifications written in the Assertion Definition Language (ADL) [SH94], a predicate logic-based language that is used to describe the relationships between inputs and outputs of a program unit. Our technique is fully automatable, and we are currently implementing a tool based on the techniques presented in this paper.