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

RT Tester Engine

Abstract Machine Layer
Communication Control Layer

Repeater

local 10BaseT Ethernet

serial 2 interface serial 1 interface

Interface
Modules

FTC-TE BTS MBSU

.......

FTC

... LANE 1 LANE 2 LANE 3 ... LANE 4

redundant bus wires are
not shown!

MIL-BUS (4 * BC, 2 * RT)

Location: DASA Test Laboratory

Fig. 4. FTC hardware-in-the-loop test conguration.

4.4 Dealing with Undened Application Layers

As an example of the application of Formal Methods for the development of
test strategies, we sketch how the problem of undened application layers was
solved for FTC testing 7 : Conceptually { though physically residing inside the
computer hardware of the system under test { the test application layer is a
part of the system's test environment, the system under test itself comprises the
hardware, the operating system and the application services. For FTC testing,
this means that the system under test consists of the four FTC hardware lanes
in conjunction with the AVI, FML and ASS software layers. We will now present

7 Further examples have been described briefly in [23].