Deriving Specifications for Systems That Are Connected to the Physical World - Formal Methods and Hybrid Real-Time Systems - page 369

Although such formal methods are not universally practised, their existence
shows that a class of errors can be eliminated from program design. Methods
which use a posit and prove approach are particularly useful because they com-
bine the predisposition of an engineer to introduce decisions one at a time with
the possibility to verify one design decision before moving on to base further
work on that decision. Such approaches use the essential ideas of redundancy
and diversity and thus minimise the amount of scrap and rework.
A development method that can scale up to deal with realistic problems must
be compositional in the sense that the specification of a subsystem is a complete
statement of its required properties. For sequential programs, various forms of pre-
condition and postcondition specifications satisfy this requirement. For concurrent
programs, the task of finding tractable compositional methods has proved more
challenging; but even here, techniques like rely and guarantee specifications (see
[Jon96, further references therein] and [MH92,BS01]) offer compositional methods.
It is worth emphasising the difference in nature between rely and guarantee
conditions because it clarifies their use in our approach. Guarantee conditions are
obligations on the code that is to be created: the program is obliged to behave in
a certain way. Rely conditions give permission to the developer to ignore possible
uses: the program is under no obligation if it is used in an environment in which
the rely condition is not true. There is of course an exact correspondence here
with preconditions and postconditions: the precondition on a square root function
tells the developer that -since the input can be assumed to be positive- imaginary
number results are outside the scope; but for positive numbers, the bounds on the
accuracy of the result must be respected by any valid implementation.
Since, in general, a program cannot directly monitor or control all the phe-
nomena of interest in the problem world, satisfaction of the customer's require-
ment must be achieved indirectly, relying on causal properties of the problem
world. We therefore use rely and guarantee conditions in the following way. The
machine and the problem world are related by mutual rely and guarantee condi-
tions: each one guarantees to satisfy certain conditions provided that it can rely
on the guarantees of its partner. On this basis we can prove that the parallel
composition of the machine with the problem world satisfies the specification
of the whole system. The rely and guarantee conditions remain explicit in the
specification documents as a reminder and a warning: they must be checked for
safe deployment.
Properties of a control system must, in general, be specified over time inter-
vals: in particular, the time interval, and its subintervals, over which the system
operates. In addition, properties may relate behaviour in one subinterval to be-
haviour in an adjoining interval. We follow the approach of explicitly quantifying
over such intervals [MH91b,MH92] (the notation is similar to the Duration Cal-
culus [CHR91]).

1.4 Fault Tolerance

Armed with the technical ideas of the previous section, it is possible to undertake
the approach of deriving specifications of the silicon package from a description