A rely–guarantee discipline for open distributed systems design

A number of authors have studied the design of distributed systems considering the existence of an environment over which little (if any) control is retained. Perhaps the most systematic of these studies suggest the use of rely and guarantee conditions that assert respectively what is assumed from the environment and what the system is committed to insure as long as the assumptions hold, a refinement of the pre- and post-conditions adopted in sequential program design. We propose a new rely–guarantee discipline based on linear time future temporal connectives and show how it can be applied in the design of open distributed systems.