Verifying consistency and validity of formal specifications by testing

Detecting faults in specifications can help reduce the cost and risk of software development because incorrect implementation can be prevented early. This goal can be achieved by verifying the consistency and validity of specifications. In this paper we put forward specification testing as a practical technique for verification and validation of formal specifications. Our approach is to derive proof obligations from a specification and then test them, in order to detect faults leading to the violation of consistency or validity of the specification. We describe proof obligations for various consistency properties of a specification, and suggest the use of Eve strategies for testing them. We provide a method for testing implicit specifications by evaluation rather than by prototyping, and criteria for interpreting the meaning of test results.