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

[11,12,19]. Incorporation of the notion of testing into the framework of Formal Meth-
ods, and the refinement calculus in particular, has been accomplished by Aichernig [1].
Testing the kind of system considered here, specifically to reactive systems, has been
the subject of a Dagstuhl meeting [4].
In outline, the paper proceeds as follows. In Section 2 a case study is presented of
a web-based network-management system, and in Section 3 the manner in which it
is linked to an implementation is discussed. Then three kinds of functional property
are considered for the generation of extra-specification tests, in Sections 4, 5 and 6.
In Section 7 a non-functional property, security, is considered. The case study is used
illustratively throughout.

2 Case Study

This section describes a web-based network-management system that helps to illustrate
the key issues discussed in this paper. The system is based on a real web application,
whose testability has been determined by the interface available.
First, a brief informal overview of the system behaviour is given (Section 2.1)
and supplemented (in Section 2.2) with a formalisation in ObjectZ. Then follows (in
Section 3) a discussion of those issues in the model that are relevant to testing; that is
followed (in Section 3.5) by a brief discussion of problems related to testability.

2.1 Overview

The system consists of a simple web-based system for managing a network of machines
remotely. It is based on a network of clients and their users. There are two special
kinds of user: administrators and managers. Although both are users, no user is both an
administrator and a manager.
The system requires users to authenticate themselves by logging on in the usual man-
ner. For security purposes, three consecutive unsuccessful logins result in the user's ac-
count being locked; this level of abstraction overlooks the details of how that is undone
by a manager or administrator). A user can log on to only one client at a time.
An administrator (and only an administrator) can create a client, provided it is not
already present and provided that a manager is assigned to it. An administrator can re-
move a client, provided there are no users logged on there. An administrator can select
a client and see its details, consisting of the client's manager and the users currently
logged on there. An administrator can also see the details of a user, consisting of its
password, whether it is logged on and if so where, how many consecutive unsuccessful
attempts it has currently made, and email it has sent and received. Finally, an admin-
istrator can broadcast mail to all users, and can send mail to a specific user as if from
another specific user.
A manager (and only a manager) can create a user account, provided the user is not
already registered. A manager can remove a user, provided it is not logged on, is not
itself a manager or administrator, and provided mail it has received is also removed.
After an administrator or manager logs out the functionality associated with its roles
cannot be invoked.