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

platform for software applications managing experiments performed on the ISS,
and for control software used during the assembly phase of the station and for
the purpose of re-boost operations. The DMS-R core component is the fault-
tolerant computer FTC. The FTC overall architecture consists of three or four
lanes (each lane is a separate computer sub-system) operating according to the
principle of active redundancy (see Figure 1): the lanes perform their tasks in a
synchronised way, and state information is kept consistent between lanes. Each
DMS-R application implemented on the FTC runs on all four lanes in parallel;
it communicates with other systems in the ISS via six independent MIL-STD
1553 busses.
Below the applications layer, each of the four lanes is structured into an ap-
plication services layer (ASS), a fault management layer (FML), and the avionics
interface (AVI). Applications and the ASS reside on a computer board using a
customised SPARC-type CPU specically manufactured for space applications
by Matra. The VxWorks operating system is used for the scheduling of ASS tasks
and applications and for resource management. Applications are programmed in
C. Both FML and AVI reside on separate transputer boards. The OCCAM pro-
gramming language has been used for the implementation of FML and AVI
software.
The AVI interfaces to the six MIL-STD 1553 busses. This bus type supports a
master (bus controller) and slave (remote terminal) concept and allows synchro-
nised data transmission/acquisition. The AVI implements a bus controller mode
for four busses and a remote terminal mode for the remaining two. Moreover, the
AVI manages a time-tagged frame protocol layer on top of the MIL-STD 1553
protocol which has been specied for global use within the ISS.
The purpose of the FML is twofold:
{ The FML provides the interface between the ASS and AVI of one lane,
transferring messages from AVI to ASS and vice versa. For communication
between ASS and FML, a VME Bus interface is used; communication be-
tween FML and AVI is performed on transputer links.
{ The FML performs the data transfer between lanes, thus allowing communi-
cation between the fault management layers of all lanes. This communication
is the basis for error detection, error correction, lane isolation (in the case of
an unrecoverable error), and lane reintegration. For this inter-lane commu-
nication, transputer links called cross strapping links are used: the FML of
each lane is connected to the FMLs of all other lanes.
To reach unanimous decisions among correctly operating lanes and as a means
for error detection, a two round Byzantine distribution schema introduced by
Lamport [13] is used, where data is communicated between FMLs and voted
using various voters specialised on dierent types of data. The objective of the
protocol is to ensure that
1. All ASS instances of non-faulty lanes get identical messages from FML,
2. All AVI instances of non-faulty lanes get identical messages from FML,