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

Methods and Tools. The time-independent verication goals deadlock freedom,
livelock freedom and correct implementation of Byzantine agreement protocol
were modelled with untimed CSP using various semantic models described by
Hoare and Roscoe [12,24] 2 . Verication of sub-system properties was performed
by model checking of renement conditions using the

FDR -tool [9]: The FDR -tool

compares pairs of CSP processes ( P 1 ; P 2 ) and checks whether a CSP renement

relation holds between the two. For compositional reasoning and to check the
applicability of specic abstraction techniques, manual proofs were worked out
and cross-checked in the project team. Code verication for the sequential voting
algorithms was performed using Hoare-style reasoning with pre-/postconditions.
Here, the

tool [4] could be applied, but some proof obligations had to
be discharged by manual reasoning. The simulation for performance analysis was
based on Generalised Stochastic Petri Nets (GSPNs) and supported by the tools
DSPN-Express

PAMELA

(see Schlinglo [30] for an introduction). Finally, real-
time tests were specied with Timed CSP interpreted in the semantics given by
Schneider [26] and executed and evaluated using the

and TimeNet

RT-Tester tool.

Overview. In Section 2, the FTC is introduced in more detail. Section 3 de-
scribes our formal verication approach, Section 4 describes the test activities
and presents the basic concept of the tool. In the nal Section 5, we

give a detailed discussion of the results obtained during the whole verication,
simulation and test suite and describe some trends in the eld of verication and
test which { according to our estimation { will become important in the future,
in order to cope with increasingly complex systems and to improve the eciency
of verication and testing.
Since this article is intended as an overview and evaluation of the verication,
simulation and test suite performed, we only give small examples to illustrate
specic aspects of our approach. A more detailed description for the dierent
topics can be found in Peleska [31] (detailed description of the FTC), Buth
et.al. [5] (deadlock analysis), [6,7] (livelock analysis), Peleska et.al. [27] (detailed
description of abstraction methods and verication of the Byzantine agreement
protocol), Schlinglo [30] (load analysis using GSPNs) and Buth et.al. [3] (e-
cient use of generic theories in the verication of fault-tolerant systems).

RT-Tester

2 Engineering Background: ISS, DMS-R and the

Fault-Tolerant Computer FTC

In its nal construction stage, the International Space Station ISS will consist of
several modules developed by dierent nations. For the Russian service module,
DaimlerChrysler have developed hardware and system software for the central
data management system, called DMS-R. The DMS-R provides an operational
2 It is assumed in this article that readers are familiar with the basics of CSP notation
and semantics. If this is not the case, Hoare and Roscoe [12,24] are recommended
as comprehensive descriptions of untimed CSP, and Schneider [26] gives a quick
introduction into the timed aspects.