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

a sequence of various product assurance tasks for the FTC. The main objectives
for this contract were:
{ Maximise the condence into the overall correctness of the FTC by perform-
ing additional verication, simulation and test tasks complementary to the
activities already carried out by the DASA product assurance team and the
software developers.
{ Let some of the most critical product assurance activities be performed by
an independent party, as is recommended by various development standards
in avionics and space technology (JP Software-Consulting/Veried Systems
and BISS are independent institutions without organisational links to Daim-
lerChrysler).
{ Increase the eciency of critical product assurance activities by using auto-
mated verication, simulation and test methods based on formal specica-
tions.
Complexity Problems. To reach these objectives, two complexity problems had
to be overcome: rst the main objective \maximise the overall correctness" had
to be structured into a collection of correctness requirements which could be
handled in a systematic way. It should be emphasised that a system of this
complexity cannot be completely specied by a set of formal specications in a
straightforward way: the diversity and number of FTC system requirements was
so large that it would have taken several man years to formalise them. Moreover,
the possible ambiguity of informal requirements was not a major concern, there-
fore the formalisation alone would not have contributed anything to the quality
of the implemented system. As a consequence, the verication suite could only
investigate a subset of requirements, and it had to be ensured that the correct-
ness aspects investigated would really cover the critical features of the system.
Second, the size of the system (about 24,000 lines of OCCAM programming code
and related detailed design specications had to be analysed in the formal veri-
cation activities performed during the whole suite, additional code was covered
in the tests) was obviously too large to be treated formally as one chunk in for-
mal specications and verications. Therefore, it was essential to nd strategies
how to decompose the system, verify small portions and combine the verication
results to conclude whether the full system met a correctness requirement or not.
Structured Correctness Requirements. Among the wide spectrum of possible cor-
rectness requirements, the following have been identied to be the most impor-
tant ones for the successful operation of the FTC in the ISS:
1. deadlock freedom of the system software responsible for FTC communication
and fault management,
2. livelock freedom of the same software,
3. correct implementation of the voting algorithms used to detect corrupted
data originating from a faulty FTC component,
4. correct implementation of the Byzantine protocol (see Lamport [13]) used
to reach agreement among non-faulty FTC components,