Specifying distributed applications: the limits of formality

Fergus, Edward Joseph (1990). Specifying distributed applications: the limits of formality. PhD thesis The Open University.

DOI: https://doi.org/10.21954/ou.ro.0000fc46


This investigation considers the use of formal specification in achieving demonstrably correct programs in the application area of distributed communication protocols. A major consideration is the factors (both theoretical and practical) which limit the value of the formal approach.

A formal specification consists of abstract mathematical objects. It can be build up systematically by assembling several smaller specification components into an overall specification, and is amenable to rigorous analysis. Three approaches to formal specification are considered: state- space, predicate calculus, and process algebra. These approaches are represented by the finite-state, Z and CSP techniques respectively. These approaches are compared in their description of protocol properties and in their amenability to rigorous analysis.

The principal conclusions are: (1) the concept of state is fundamental to communication protocols, and the finite-state approach to protocol specification is as powerful as predicate calculus and process algebra; (2) a novel technique is developed to enumerate global-state trees economically; (3) modal logic is necessary in a Z specification which addresses questions of liveness and eventuality; (4) the semantic completeness of some CSP constructions is questionable; (5) the concept of fairness in finite descriptions of behaviour is given a rigorous definition; (6) a system specification should be operational in character; (7) a formal specification technique is essentially functional in the narrow mathematical sense; (8) non-functional requirements are invalid elements of a demonstrable specification.

Viewing alternatives

Download history


Public Attention

Altmetrics from Altmetric

Number of Citations

Citations from Dimensions

Item Actions