Testability of Formal Specifications

Abstract In the SPECS project (RACE 1046) formal methods for testing were applied on a existing Integrated Broadband Communication system. This paper reports on experience gained in this exercise. It focuses on properties of formal specifications that are indispensable or desirable when the specification is to be used as a basis for testing. The problems encountered in the exercise can be considered aspects of the relation between system specifications and their implementations. A short survey of existing theory on this topic is presented. It is concluded that, although the theory discussed is not capable to provide a full solution, it shows a direction to go. Recommendations how to write formal specifications that are more suitable as a basis for testing are given.