Copy the page URI to the clipboard
Fergus, Edward Joseph
(1990).
DOI: https://doi.org/10.21954/ou.ro.0000fc46
Abstract
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.