The idea of the Hayes/Jackson/Jones approach is simple: for many technical systems it is necessary to derive their specification from one of a wider system in which physical phenomena are measurable. Even though the computer itself cannot affect the physical world directly, it is still worthwhile to start with the wider system. The message can be stated negatively: don't jump into specifying the digital system in isolation - start by recording the requirements of a wider (physical) system. The following picture might help.

In order to be able to write the necessary specifications in the Hayes, Jackson, Jones style, some technical work derived from earlier publications of the three authors has to be brought together. The process of deriving the specification of the software system involves recording assumptions about the non-software components. These assumptions are recorded as rely conditions because we know how to reason about them from Jones' earlier work on concurrency. In most cases, we need to reason about the continuous behaviour of physical variables like altitude: earlier work by Hayes (and his PhD student Mahony) provides suitable notation. The emphasis on ìproblem framesî comes from Jacksonís recent publications.

The simplest example of the HJJ approach is a computer-controlled temperature system: rather than start by specifying the digital controller, an initial specification in terms of the actual temperature should be written; in order to derive the specification of the control system, one needs to record assumptions (rely conditions) about the accuracy of sensors and about the fact that setting digital switches results in a change in temperature. Once the specification of the control system has been determined, its design and code can be created as a separate exercise. At all stages (but particularly before deployment) someone has to make the decision that the rely conditions are in accordance with the available equipment.
The referenced [hjj03] outlines this procedure for a "sluice gate" controller. The analysis includes looking at tolerating faults by describing weaker guarantees in the presence of weaker rely conditions.

Notice that it is not necessary to build a complete model of the external components like motors, sensors and relays: only to record assumptions. But even in the simple sluice gate example, it becomes clear that choosing the perimeter of the system is a crucial question: one can consider the physical phenomena to be controlled as the height of the gate, or the amount of water flowing; or the humidity of the soil; or even the farm profits. Each such scope results in different sorts of rely-conditions.