ENGINEERING FORMAL REQUIREMENTS - AN ANALYSIS AND TESTING METHOD FOR Z-DOCUMENTS

Z is a declarative, non-executable specification language; its diffusi on in the field of requirements engineering outside academia is slow b ut growing. In this paper we focus on some methods for analyzing and t esting Z specification documents, with special emphasis on non-sequent ial systems specifications. We describe two techniques we have adopted : the former allows the specifier to add to the requirements document a number of properties that then can be checked using a formal semanti cs; the latter makes it possible to build directly from the requiremen ts specification document a distributed prototype which can be execute d and tested over a network of workstations.