Formal methods for the International Space Station ISS

This article summarises and evaluates the results and experiences obtained from a verification, simulation and test suite for a fault-tolerant computer system designed and developed by DaimlerChrysler Aerospace for the International Space Station ISS. Verification and testing focused on various aspects of system correctness which together ensure a high degree of trustworthiness for the system. The verification and test approach is based on CSP specifications, the model-checking tool FDR and the test automation tool RT-Tester. Furthermore, Generalised 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, motivate and evaluate our approach that strongly relied on the combination of different methods, techniques and tools in order to increase the overall efficiency of the verification, simulation and test suite. The isolated techniques applied are illustrated by small examples; for details, references to other publications are given.