Specification for Testing - Formal Methods and Hybrid Real-Time Systems - page 296

observable no = 0 , 3, on both values of any Boolean variable, on the initial values of the
set State observables, on the empty and full cases of post , and so on.
The specifier is in a position to define appropriate boundary functions, which the
tester might not think of. For that purpose it is sometimes easier (compared with the
method used in [24]) to define an order (like set inclusion or ordering on integers) and
to identify a boundary with its extreme points. That yields all the examples mentioned
above.
One interesting, less systematic, example already considered is identification of a
dummy user to include as a boundary point, as discussed in Section 3.5. But this is
information a specifier has only if familiar with the test constraints.
Another example is provided by the important operation of logging in. There are
potentially infinitely many ways in which the login operation can yield Fail . Of course
in testing, a suitable subset of inputs must be found to trigger that behaviour. However,
the model does not explicitly state which inputs to consider. Again, it is appropriate for
the specifier to augment the specification with information to aid testing. For instance,
a suitable function f can be defined with the property that if Login(u?,id?) succeeds
then Login(u?,f(id?)) should fail.
Similarly, tests Login(ux,idx) can be generated where ux is not a valid user, by
specifying rules for ux . Such tests should of course fail for any value of idx ,and
rules for choice of idx can be specified. An alternative is to specify sets Uinvalid and
Pinvalid and generate all tests for

( ux , idx ) : Uinvalid × Pinvalid .

7 Intermediate States

So far only functional properties, like those exemplified by Webbo , have been consid-
ered. But it is important for a specifier, and tester, to take account of so-called 'non-
functional' properties like security, non-interference, distribution and even efficiency.
This section considers one common situation that is typically a source of insecurity in
the sense of exposing information that ought to remain concealed.

7.1 Sequential Components

The linking of the code to the model implicitly involves different levels of atomicity.
It may be convenient, for example, to implement an operation op with a sequential
composition op = op 0 9 op 1where op 0 is responsible for some of the I/O and op 1for
the others. However such a factorisation may result in a security leak.
For example, the login operation of Webbo assumes that the system responds, atom-
ically, only after both the user name and password have been input and the login button
has been clicked. But in some implementations, login could be achieved as the se-
quential composition of two 'sub'-operations the first of which provides the user with
information about the success of part of the process. If that information ought to be
secure, then this factorisation of login should be flagged as a security hazard.
More explicitly, login may be expressed as a check that the user identified by input
u ? is valid, i.e. u ? ∈ U , (with no output but with a Boolean variable to record ( u ? ∈ U )