Information Technology Reference
In-Depth Information
Formal Methods for the International Space
Station ISS
Jan Peleska 1 ; 2 and Bettina Buth 1
1 TZI-BISS, University of Bremen, EMail f bb,jp g @tzi.org
2 Veried Systems International GmbH, Bremen, EMail jp@veried.de
Abstract. This article summarises and evaluates the results and expe-
riences obtained from a verication, simulation and test suite for a fault-
tolerant computer system designed and developed by DaimlerChrysler
Aerospace for the International Space Station ISS. Verication and test-
ing focused on various aspects of system correctness which together en-
sure a high degree of trustworthiness for the system. The verication
and test approach is based on CSP specications, the model-checking
tool FDR and the test automation tool RT-Tester . Furthermore, Gen-
eralised Stochastic Petri Nets (GSPN) have been used with the tools
DSPN-Express and TimeNet to perform a statistical throughput analysis
by means of simulation. The objective of this article is to present, moti-
vate and evaluate our approach that strongly relied on the combination
of dierent methods, techniques and tools in order to increase the overall
eciency of the verication, simulation and test suite. The isolated tech-
niques applied are illustrated by small examples; for details, references
to other publications are given.
Keywords: Fault-Tolerant Systems | Byzantine Agreement Protocol
| Formal Verication | CSP | Test Automation | Model Checking
| Generalised Stochastic Petri Nets | Hardware-in-the-loop Test |
International Space Station
1
Introduction
Objectives. This article is intended as a summary and an evaluation of a verica-
tion, simulation and test suite performed in several steps between 1995 and 1998
for a fault-tolerant system to be integrated in the International Space Station
(ISS). The system inspected during this suite is the 4-redundant Fault-Tolerant
Computer (FTC) which is the main component of the Data Management Sys-
tem (DMS-R) developed by DaimlerChrysler Aerospace (DASA) for the Russian
module of the ISS. More details about the FTC, including an overview of the
FTC hardware and software architecture are given in Section 2.
The verication, simulation and test project started in 1995 when JP Software-
Consulting (now Veried Systems International GmbH) in collaboration with the
Bremen Institute of Safe Systems (BISS) were contracted by DASA to perform
Search WWH ::




Custom Search