Information Technology Reference
In-Depth Information
an application layer is dened in the programmers' reference manual specifying
{ at least in a semi-formal way { the interfaces and restrictions for the usage of
all system services available to an application. Furthermore, restrictions regard-
ing the maximum CPU load which may be created by applications are described
there. As a consequence, the most general behaviour of an admissible application
can be derived from the programmers' reference manual and serve as input for
the design of the TASL. Observe however, that as long as the reference manual
is an informal document, the derivation of the TASL from such a manual is a
process which cannot be automated and depends on the technical insight of the
specialists performing this process. As a consequence, the TASL design has to
be validated carefully in order to justify the claim that the possible behaviours
of every concrete admissible application layer will form a subset of the TASL
behaviour.
For FTC testing, the dierent variants of TASL behaviour were controlled by
the test engine: abstract machines running in the AML used MIL bus messages to
transfer commands to the TASL. As a consequence, the expected FTC behaviour
was known in the test engine at every point in time, so that evaluation of observed
FTC behaviour against expected behaviour could be performed automatically.
The FTC TASL activities can be roughly classied as follows:
{
Data transmission and reception with variable length on the various com-
munication channels available to the FTC application layer,
{
Simulation of exceptional application behaviour, such as creation of commu-
nication overloads (to test FTC robustness in overload situations), corrup-
tion of data packages and creation of timing jitters on isolated lanes (to test
fault detection capabilities of the FML voters),
{
Control of FTC lane re-integration after occurrence of a lane fault,
{
Control of redundant bus wires.
5
Discussion
5.1
A Summary of Verication, Simulation and Test Results
In the subsequent paragraphs, an overview of results obtained during the veri-
cation, simulation and test suite described above is presented. More details may
be found in [5,6,30].
Verication of Deadlock and Livelock Freedom.
The deadlock analysis for the
AVI layer was performed at the stage when the transition from detailed design
to coding had just been completed and the rst informal tests were carried out
by the development team. In this phase, 7 deadlock situations were uncovered
during our verication suite. Only two of these errors were detected by the de-
velopers' tests, since the traces leading to the other deadlock situations involved
complex communication and scheduling patterns which only occurred in rare
situations. As a consequence, the probability of running into these situations
during informal testing was quite low. Using the
FDR
-generated example traces
Search WWH ::
Custom Search