Communication in Processor Farms: A Case Study in Reactive Systems Refinement

We study the formal derivation of a distributed system that models the behaviour of an arbitrary processor farm. A processor farm is a reactive system that consists of a unique master processor together with a number of identical slave processors connected via a communication network. The system reacts with its environment that requires certain service from the farm through the master processor. We focus on the design of the communication network, which is stepwise brought about. We show how a combination of action systems and refinement calculus gives us a uniform method for deriving such a reactive system. 1 Introduction A processor farm [10, 15] is a distributed system that consists of a unique master processor together with an arbitrary number of identical slave processors connected via a communication network. We assume that there is an environment that generates some tasks that the farm is required to solve. The tasks are given to the master that distributes them to the slaves f..