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

It could be shown by model checking that for each communication cycle in the
network of sub-systems shown in Figure 1, at least one sub-system is a renement
of a MUXCON instance dened with N = 0. Since deadlock freedom is preserved
under renement and renement distributes through the parallel operator, this
established deadlock freedom for the full FML layer.

t
The above example is only one type of compositional reasoning and generic
theory applied in the FTC verication suite. Additional methods have been
described by Buth et.al. [3,5,6,7].

4 Test Automation Techniques

4.1 Test Objectives
As explained in Section 1, the objective of the test suite was to complement
the verication and simulation activities. As a consequence, we did not perform
unit or integration tests on software level (these had been performed by the
development team in earlier stages of the projects), but designed and executed
a hardware-in-the-loop test suite, with an FTC engineering qualication model
(EQM) as system under test . An EQM consists of the original hardware as it
will be used in space, with the original flight software integrated on the comput-
ers. The test objective was to investigate the correctness of hardware/software
integration, and the test concept had the following characteristics:
{ All relevant aspects of FTC functionality were tested in parallel, so that
hidden dependencies between dierent functional components of the AVI,
FML and ASS software layers could be detected.
{ Each functional aspect was tested with respect to normal behaviour (all
environment components act as required) and exceptional behaviour (some
environment components provide corrupt data, show timing jitters etc.).
Normal and exceptional behaviour test phases were interleaved with each
other. Exceptional behaviour tests for one functional aspect could occur in
parallel with normal behaviour tests for other aspects.
{ Tests were executed in non-stop fashion, so that the FTC dependability could
be investigated over long operational time intervals. Even the occurrence of
errors should not stop the test as long as at least one FTC lane remained
operational. It was a major test objective that lanes which failed due to a
fault injection or due to an unexpected error should be re-integrated into
the system in an automatic way.

Apart from the check of various functional features of the FTC system ser-
vices, the tests had to investigate specic properties related to communication
throughput:
{ Keeping of the nominal and maximum data throughput under various bus
load proles 5 ,
5 A load prole distributes a given throughput (e.g., 60KBytes/sec) in a specic way
on the protocol frames which are transmitted per time unit. The FTC services time
frames at a rate of 80Hz, and each frame may transport up to 408 16-Bit words.