Information Technology Reference
In-Depth Information
Other users have very limited capabilities (at this level of abstraction). They can log
in on any client, read their messages and send messages to other users and log out. But
they cannot manage users or clients.
Initially there is at least one administrator and at least one manager (just because this
level of abstraction abstracts the actions that change those sets), there are no other users,
no user is logged in nor has tried to log in, and there is no post. It is arbitrary where the
administrators and managers are initially logged in.
2.2
Model:
Webbo
The model of that web-based network-management system is called
Webbo
. The speci-
fication below is approximately ObjectZ [8] but uses dependent types in order to shorten
schema invariants and uses
C
D
to stand for the disjoint union of
C
and
D
(
i.e.
the
union in which the invariant
C
holds).
These generic types are assumed:
Users
for the set of possible users;
Clients
for the
set of possible clients;
Mess
for the set of email messages; and
Pa ss
for the set of all
possible passwords, both valid and invalid (thus
Pa ss
might well consist of the set of all
character strings constrained in some way by length; but such detail is ignored at this
level of abstraction).
These schemas are required and defined in the specification.
Loginfo
provides for
each user: the number
no
of putative logins in the current sequence of attempts by that
user; the user's password
pd
; a Boolean
in
which is true iff the user is currently logged
in; the client
at
at which, if
in
is true, the user is logged in; and a Boolean
lock
which is
true iff the user's account is locked (thus
lock
is a redundant observable, equivalent to
(
no
= 3)).
State is described by sets:
U
of users,
A
of system administrators,
M
of managers
of clients,
C
of clients; by a function
mng
which assigns a manager to each client (so
is a total function), a function
log
which assigns
Loginfo
to each user, and a relation
post
between a sender-receiver pair and messages that is in general many-to-many. See
Figure 1.
An administrator can create a client, with operation
CreateClient
, only if logged
in, the client is not already in the network, and by assigning a manager to the client.
Removal of a client, by operation
RemoveClient
, is similar, except that for a client to be
removed it must have no users logged in there. See Figure 2.
With operation
AdminClient
, an administrator
a
? can receive information about the
manager
man
! of a client
c
? and about which users,
users
!, are logged in there. With
operation
AdminUser
an administrator can receive information about a user
u
?. See
Figure 3.
An administrator
a
? sends post either by broadcasting a message
p
? to all users from
itself, with operation
AdminPostAll
, or by sending it to just a single recipient
r
? from
user
u
?, with operation
AdminPostOne
. See Figure 4.
The 'management' of users extends that of clients, because when a user is removed
by a manager, its email is also removed; the user must not be logged in, and must not
be an administrator or manager. This description abstracts the initial choice of a client's
password. See Figure 5.
∩
D
=
{}
Search WWH ::
Custom Search