Stepwise development of fair distributed systems

A theory of fairness which supports the specification and development of a wide variety of “fair” systems is developed. The definition of fairness presented is much more general than the standard forms of weak and strong fairness, allowing the uniform treatment of many different kinds of fairness within the same formalism, such as probabilistic behaviour, for example. The semantic definition of fairness consists of a safety condition on finite sequences of actions and a liveness or termination condition on the fair infinite sequences of actions. The definition of the predicate transformer of a fair action system permits the use of the existing framework for program development, including the existing definitions of refinement and data refinement, thus avoiding an ad hoc treatment of fairness. The theory includes results that support the modular development of fair action systems, like monotonicity, adding skips, and data refinement. The weakest precondition and the weakest errorfree precondition are unified, so that in particular a standard action system is a special case of a fair action system. The results are illustrated with the development from specification of an unreliable buffer. Received: 3 January 2000 / 17 November 2002