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

different. When login succeeds, the web page has the menu item with the appropriate
functionality; whilst if the login fails, the web page does not have the menu item but
goes back to the retry page (that is, until the user is locked out). This again assumes
availability of the appropriate methods to inspect the resulting web page.

3.4 Link Issues for Testing

The model exhibits the behaviour that three consecutive loginFail(i,_) result in
locking the user's account. To build the oracle into the action word, one might use
loginLock(i,p) . Again the link has to translate the login process as before, but with
a different check on the outcome.
The implementation may have state variables such as Booleans auth and lock
which may not be directly accessible from the web page. In this particular case the
implementation generates output on the web page by setting the title to “Not Logged
in” or “Logged in”.
If the link has only a method to examine the title, it is not possible to determine if
the account is locked. That is, both loginFail(i,p) and loginLock(i,p) may be
forced by the link into checking the title to “Not Logged in”.
Either the title has to change or a method to examine locked is essential. If there
were a message displaying 'locked' then the web page can be tested by checking its
contents.
Sometimes there are popups (say created by Javascript) that require confirmation. In
the model there are transitions of the form clickOK . They need to be translated into
a number of operations—getting a handle of the javascript window, clicking the okay
button there, waiting for that window to disappear and the main window to go to the
desired page.
Usually all, or anyway most, of the methods are available or can be made available
but if the web page does not provide that information, testing fails.

3.5 Problems with Test Automation

The purpose of this section is to show that developing a model and a link from the
model to the implementation cannot automate all aspects of testing. The standard black
box testing approach to web systems is thus not sufficient.
The first problem arises since an administrator can send, with operation AdminPos-
tOne , a message on behalf of a user. The precondition for this operation is that the user
posting the message should be an administrator and the message should be addressed
to an existing user from an existing user. The model also defines the expected result of
the operation: the message should be added to the pool of messages (various designs
for which are discussed in Section 5.6).
Assume that an administrator a posts a message on behalf of the user u to r .After
posting the message the system returns a to the web page from where the messages can
be managed. Administrator a has no direct way of verifying that the message has been
added to the post. That is, it is not possible to define a link using the methods made
available by the web system.