Information Technology Reference
In-Depth Information
Logout
Δ(
log
)
u
?:
U
log
(
u
?)
.
in
¬
log
(
u
?)
.
in
log
(
u
?)
.
pd
=
log
(
u
?)
.
pd
log
(
u
?)
.
no
=
log
(
u
?)
.
no
∀
v
:
U
·
v
=
u
?
log
(
v
)
=
log
(
v
)
⇒
Fig. 8.
Logging out in
Webbo
Webbo
Webbo
State
ClientManagement
AdminClient
AdminUser
AdminMail
UserManagement
UserMail
LoggingIn
Logout
Fig. 9.
The overall system
Webbo
Logging out is straightforward and is described in Figure 8. User
u
? is logged in
before the operation but not after it; its password remains unchanged as does its number
of unsuccessful login attempts (at 0); however
log
(
u
?)
.
at
is left arbitrary.
Overall
Webbo
is specified with a class that combines the previous descriptions; see
Figure 9.
3
Linking Model to Implementation
This section outlines how the link between the model and the implementation can be
developed for the purposes of testing. Several examples are presented to illustrate the
main issues, since a complete description lies beyond the scope of this paper.
3.1
Testing Language
General purpose programming languages are in general used to test systems (
e.g.
,Java
is used in the Korat framework [3] and Ruby/Watir is used for testing web based sys-
tems [16]). This ensures that the expressive power of the tester is not restricted. But the
Search WWH ::
Custom Search