Information Technology Reference
In-Depth Information
5. meeting of the performance requirements dened for the FTC network in-
terface,
6. correct FTC behaviour in presence of exceptions, that is, correct isolation
of faulty components, consistent re-conguration of remaining components
and consistent re-integration of repaired ones,
7. correct integration of system software on the customised computer and com-
munication hardware which has been specically designed for space missions.
Selection of Methods.
The correctness requirements 1 | 4 are obviously inde-
pendent of the underlying hardware, therefore it was decided to analyse the FTC
software by means of formal verication techniques. The starting point for these
verications were the FTC detailed design document and the software code. For
the performance requirements 5, not only the concrete throughput gures which
could be obtained with the FTC were of interest, but also the impact of certain
design decisions on the communication performance. Therefore it was decided to
analyse throughput properties in two ways: (1) Simulations based on the soft-
ware design and on the known performance properties of the hardware: here the
main objective was to study the impact of design decisions on performance; (2)
Hardware-in-the-loop tests
1
with the complete FTC hardware and software to
check the quantitative performance values. Requirements 6 and 7 are related to
hardware/software integration, therefore it was decided to analyse the respective
FTC behaviour in hardware-in-the-loop tests.
Verication Strategy.
To tackle the complexity problem presented by the sys-
tem size, a verication approach was elaborated, combining the following four
fundamental methods:
{
Abstraction methods
transforming program code or detailed design speci-
cations into simplied formal specications which could be analysed with
respect to accordingly transformed requirements, such that correctness on
formal specication level implied correctness on code/design level.
{
Model checking of renement relations
to prove local properties of small
sub-systems.
{
Compositional reasoning
to deduce overall system correctness from local
properties of small sub-systems.
{
Generic theories
to re-use correctness results which only depend on generic
characteristics of (sub-)systems; these can be applied to instance processes
belonging to the same generic class.
This approach is described in more detail in Section 3.
1
These tests are used to investigate the correct behaviour of integrated hard-
ware/software (sub-) systems: Tests are driven by separate computer components
stimulating the system input interfaces and evaluating the system behaviour by ob-
serving its output interfaces. This results in closed-loop test congurations consisting
of the system under test and the test driver.
Search WWH ::
Custom Search