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

of the verication is very high for the FML software. For technical reasons, the
AVI layer could not be designed with such simple patterns. As a consequence,
the deadlock and livelock analysis results obtained for the AVI should rather be
regarded as a \sophisticated test suite" which after having uncovered a number
of errors did not nd any new ones. However, it should be emphasised that the
quality of these \tests" is much higher than what could ever be achieved by
systematic but informal design reviews because of the high number of states
explored during the model checking process.
The verication eort was much smaller for those parts of the system where
standardised design patterns had been used by the software developers.
Simulation. The simulations could not predict the existence of specic load pro-
les causing problems for the AVI although the average load was still below
the maximum load gure. This is due to the fact that several simplications
regarding the underlying AVI hardware had to be used in the GSPN model in
order to make the simulation feasible and to keep the modelling costs within
acceptable bounds. In cases where the detailed behavioural specications of spe-
cic hardware components and the source code of o-the-shelf software used in
the system implementation are not available, formal simulation models can only
be approximations of the true component behaviour. Therefore the simulation
results should be used as indicator which throughput aspects should be tested
more closely with the real system. In this respect, they provided an excellent
preparation for the selection of test strategies. Furthermore, simulations can be
very helpful in early design phases to decide which design variants will result in
better throughput values.
Tests. The results achieved during the hardware-in-the-loop tests obviously jus-
tify the test approach. It is noteworthy that all the critical errors uncovered
during tests were related to timing and synchronisation problems. Therefore we
would like to emphasise that testing should be understood as a complementary
activity to (formal) verication:
{ The verication activities should focus on uncovering programming bugs in
data transformations and design errors related to the cooperation of parallel
components.
{ Testing should focus on potential problems arising from the integration of
software on the hardware and on those correctness aspects where a complete
formal model could not be constructed.
As was to be expected for a system of such complexity, the test coverage achieved
was far from being exhaustive 9 . Therefore it was important to use a test strategy
9 The situation is even worse for the test of real-time systems controlling slow physical
processes or systems: since it is often impossible or not advisable to increase the
controller speed for testing purposes, the achievable coverage is simply limited by
time it needs to execute each test. As a consequence, the theoretical results how to
achieve complete coverage and how testing may \converge" to full correctness proofs
are not very helpful in this context.