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

it is important to identify those software components whose malfunction may
really endanger system safety. In a good controller design, these components will
represent only a small subset of all software modules, so formal verication and
the main testing eorts could focus on these critical modules and their interac-
tion. Hazard analysis methods can be used to identify the critical components
and to justify why other modules may be checked with less eort.
Hazard analysis is complemented by risk analysis calculating the probability
of a hazardous event and its consequences to occur [29, p. 60]. In this eld,
there still remains an important gap to be bridged between formal specication
languages and safety-critical systems engineering: while it suces for hazard
analysis to have nondeterministic constructs in the specication language { for
example, in terms like

SERVER = request ? x ! ( PROCESS REQUEST ( x ) u SERVER FAILURE )

{ risk analysis requires to associate nondeterministic alternatives with probabil-
ities, but in most formal specication languages, stochastic aspects cannot be
expressed. To our knowledge, only very few attempts to extend CSP semantics
in the direction of stochastic models have been made (see, for example [32] for
such an approach) and currently, no tool support seems to be available for such
models. As a consequence, the usability of CSP cannot be extended to risk anal-
ysis, to stochastic load analysis or to the development of test strategies based on
stochastic models. For these reasons, we regard stochastic extensions for Timed
CSP and similar formal specication languages to be of high importance to im-
prove their usability in the context of safety-critical systems.

5.4 A Concluding Remark About Formal Methods and Ethics

In all the industrial verication and testing projects we have performed so far, it
was never the case that Formal Methods have been utilised to increase product
quality. Instead, they were applied in situations where adequate product quality
could be achieved with less eort { by mechanised evaluation of formal spec-
ications for verication by model checking or automated testing { than with
conventional methods. Today, cost considerations even dominate the areas of
safety-critical systems development, quality assurance and operation { the ICE
train catastrophe in Eschede 1998 being the most dramatic recent example of the
consequences of quality control driven by an emphasis on cost minimisation. We
expect that the industrial applications of tool-supported Formal Methods will
continually increase with the very objective to further reduce product assess-
ment costs. It is therefore our responsibility as scientists and practitioners not
to be carried away by the enthusiasm to advertise the benets of our favourite
methods and tools, but instead to explain the project-dependent limitations of
automated formal verication, validation and test suites in an unambiguous way.