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

In fact, the question of transience is even more delicate because the same
reasoning that causes us to recognise transience as an issue means that “si-
multaneous” actually means “within a small time interval”. It is issues like
these which have prompted the second author of this paper to consider “time
bands” [BHBF05] — see further discussion in Section 4.3.

3.7 Combining Specifications

In [Jac00], the reliability concern is normally handled by introducing new sub-
problems. The way in which such subproblems can be specified is indicated in
Sections 3.3-3.6 and within “normal design” one might use a standard pattern for
combining solutions to the subproblems. Thus the notation described in Section 2
would suce. But one would also wish to draw conclusions about combinations
of machine descriptions. In the same spirit, there are issues concerning “phases”
of operation (one example of which is the special problems that arise during
system initialisation) which prompt us to want to reason about combinations of
machine descriptions.
Thus the desire to specify a fault-tolerant system in a structured way ne-
cessitates a semantics for combinators over machine specifications. This applies
even if we consider the problem of detecting faults as a separate issue from the
“healthy” behaviour. Consider a single machine description and recall the com-
ment in Section 1.2 about the conceptual distinction between rely and guarantee
conditions (the former are to be viewed as permissions to the designer to ignore
certain potential deployments; the latter are obligations on the code created by
the designer). We should not therefore expect to find code in the program de-
veloped from this specification that will check on the truth of the rely condition.
Instead, the created program must not be deployed in contexts where the rely
condition is not satisfied. We are then obliged either to use Controller 1onlyin
situations where its inputs satisfy the rely condition or, perhaps, to ignore its
outputs where they do not.
It is however clear that, if we wish to detect faults, there might have to be
code in another subproblem which monitors the rely condition. The argument
in Section 3.2 is that the closer the rely condition of an overall system can be
made to true the more robust a system will be. Furthermore, the extra code
that is required is more complicated than the case with a simple precondition
where one only needs check a parameter: the truth of a rely condition can only
be determined over a period of time. It is the need to combine machines (de-
veloped with simple rely conditions) with machines which monitor for a healthy
environment that points to the need to be able to reason about combinations
of machine descriptions and this introduces some technical issues which require
further research (the authors are working on a further paper on this topic).

3.8 Normal and Radical Design

An aspect of system development that is less often discussed than it should be
is what Vincenti [Vin90] calls normal design . Normal design is what an engineer
does when designing a product for which there are well established standards