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

The test specication sub-system supports the development of test specica-
tions in various formal specication styles. For each formalism, specications are
translated into binary representations as generalised labelled transition systems
(GLTS) . These GLTS extend LTS as introduced by Milner [18] and others as
follows:

{ LTS nodes are annotated with acceptance sets to specify nondeterminism
(this concept has also been used for model representations in the FDR

tool [9]),
{ Multiple clocks (in the sense of timers) may be associated with LTS states by
introduction of auxiliary events to set timers and to react on elapsed timers
(this extends the LTS alphabet

by set-/elapsed timer events from a set

Timer , see Peleska [22]),
{ Each LTS is extended by a set of additional state variables from a set V (this

may be used to reduce the overall number of LTS nodes),
{ Transition labels may be specied as

LTS events e 2 ,

Auxiliary timer events e 2 Timer ,

Conditions on the values of variables v 2V ,

Conjunctions of LTS event occurrences and conditions.

The GLTS model is rich enough to encode dierent timed specication for-
malisms, such as Timed CSP [26], Timed Automata (at present, we use a vari-
ant of Timed Automata as introduced in [8]), Message Sequence Charts [1] and
Statecharts [11]. A complete test is specied by one or more specication, each
describing a dierent aspect of system under test functionality to be tested in
parallel with the others. Dierent specication styles may be combined. For FTC
testing, all test specications were written in Timed CSP, and the FDR tool was

used as an integrated component to validate CSP specications and

to transform them into GLTS representations 6 .
The

RT-Tester

core component consists of the real-time test sub-system .In
its abstract machine layer (AML) , one or more interpreters called abstract ma-
chines are executed during a test run, each abstract machine interpreting the
GLTS representation of a test specication. Depending on the semantics of the
specication language, dierent types of abstract machines are used for GLTS
interpretation. Each abstract machine evaluates the GLTS structure in real-time
to determine which inputs may be sent to the interfaces of the system under test,
which outputs are to be expected from the system under test and which tim-
ing conditions are to be observed. The GLTS graph structure is used to apply
various test strategies in order to achieve good test coverage. The timed traces
of inputs sent to and outputs received from the system under test are recorded
in execution logs which can be used for automatic test documentation and to
perform oine evaluation of specic correctness aspects.
6 The underlying theoretical foundations related to testing against CSP specications
have been described in more detail in [19,20,21,22]. Note that the prototype version
of the product was called VVT-RT.

RT-Tester