Determining a specification from context
formal specification, hayes/jackson/jonesSummary
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
written; in order to derive the specification of the control system,
one needs to record assumptions (rely conditions) about the accuracy
sensors and about the fact that setting digital switches results in a
change in temperature. Once the specification of the control system
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
the available equipment.
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.
[hjj03] Ian Hayes, Michael Jackson, and Cliff
Jones. Determining the specification of a control system from that
environment. In Keijiro Araki, Stefani Gnesi, and Dino Mandrioli, editors,
FME 2003: Formal Methods, volume 2805 of Lecture Notes in Computer
154-169. Springer Verlag, 2003.
Cliff Jones (Newcastle)
|Page Maintainer: firstname.lastname@example.org||Credits||Project Members only||Last Modified: 30 May, 2006|