Integrated Formal Methods

This article considers the problem of interpreting behavioural meanings from model-based specifications written in formal specification languages such as Z, VDM-SL or AMN. It contends that certain requirements - such as the order in which operations are invoked, the origin, destination, and ordering (together with the implied presence) of inputs and outputs - significant in certain problem domains, are difficult to express within the established approaches. In the light of this discussion we promote an approach that combines the expressive powers of both process algebras and model-based approaches for the modelling of systems with a pronounced behavioural perspective as well as significant emphasis on data and process requirements. As a first step toward an integrated language involving Z and CCS, a language, ZCCS, is presented - a dialect of value-passing CCS that employs Z as its value-calculus. The (abstract) syntax of the language is defined and a small example of a ZCCS specification is supplied.