Formal Methods for the International Space Station ISS - Correct System Design: Recent Insights and Advances - page 373

and instantiate them for the specic solutions to be constructed, getting a col-
lection of guaranteed correctness properties from the associated generic theory.
Using design patterns, it might be possible to develop systems in such a way
that the application-independent correctness properties (such as deadlock free-
dom and livelock freedom) would be automatically fullled. As a consequence,
verication could focus on the application-specic aspects. The re-usability of
generic theories associated with design patterns would justify a high eort to
be invested into the verication of these theories. Therefore, we recommend to
verify these theories with the support of proof tools (see [3] for an example of
establishing generic theories using the HOL proof tool).
The generic theories exploited in the verication suite described in this ar-
ticle focus on communication patterns. For the verication of real-time systems
new categories of patterns related to timing behaviour should be developed; for
example, it would be useful to elaborate a family of patterns and associated theo-
ries for the handling of frame protocol communication and time-frame dependent
scheduling of processes.
It remains an open question whether suciently powerful and widely appli-
cable generic theories for application-dependent design patterns { that is, frame-
works { will be established in the future. For example, in the application domain
\fault-tolerant systems" a standard design for the full Byzantine protocol might
be regarded as a framework, to be applied \o-the-shelf" as soon as mechanisms
for decision making among actively redundant computers are needed.
Formal Methods, Hazard and Risk Analysis. While hazard analysis methods
were originally used to investigate hardware failures and their impact on system
safety, it may nowadays be regarded as state-of-the-art to extend hazard analysis
to software components [17,29]. In the context of safety-critical controllers, this is
only natural, since software failures are certainly just as hazardous as hardware
crashes. Among the various techniques of hazard analysis, Fault-Tree Analysis
is of greatest value, since it allows us to consider logical combinations of local
faults and their impact on global system safety. Moreover, fault-trees can be
mechanically transformed into safety requirements for a controller. Conversely, a
formal fault-tree representation can be used to verify safety mechanisms designed
for a controller: analysing the \parallel combination" of a fault-tree model and
the safety mechanism, it can be shown by model checking that the root of the
fault-tree { that is, the hazard { can never be reached as long as the safety-
mechanism shows its specied behaviour [14,15].
A more subtle application of hazard analysis methods { specically, fault-tree
analysis { is becoming increasingly important. Fault-tree analysis and Failure
Modes and Eects analysis [29, pp. 33] are extremely useful for partial (formal)
software verication [17, pp. 615] and the design of test strategies: in most real-
world applications, complete software verication will be infeasible. Therefore
by M. Spivey [28]. However, the Z Mathematical Tool-kit corresponds to isolated
generic classes and theories about them. There is nothing equivalent to design pat-
terns in [28].