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

for use by the second sub-operation) followed by a check that if so then the password
provided is correct, i.e. log ( u ?) . pd = p ?, (with appropriate change of state and output
ack !) then an opportunity is provided for a malicious user to obtain information about
U by probing with the first sub-operation.
Assume that loginFail(u?,p?) is linked to

enter_text(:name,u?);
enter_text(:password,p?);
login.click();
check-not-logged-in();

with the assumption only that the user u? and the password p? do not tally. It is desired
also to check that if u? is not a valid user, no message is returned. To simplify the
specification of the link, loginFail(u?,p?) is split into a sequential composition

loginFailName(u?) ; loginFailPassword(p?) .

The code that links the action word loginFailName(u?) to the system is

enter_text(:name,u?);
check-no-message();

and the code that links the action word loginFailPassword(p?) to the system is

enter_text(:password,u?);
login.click();
check-not-logged-in();

An alternative solution to this problem is to have another action word
loginFailNoUser . But that complicates the specification of the model and the link
between the model and code.

7.2 Principle

In general if the code associated with an action word a is of the form b0;b1 ,

a b0;b1 ,

where b0 represents a desired behaviour in itself, it is better to split a into a0;a1 and
associate a0 with b0 and a1 with b1

a = a0;a1 ,

where a0 b0 and a1 b1 .

Similarly, if the code associated with an action word a is of the form b0;b1 where
b1 is associated with another action word b , it is better to associate a with only b0 and
change the model by replacing the a transitions with a;b transitions.