Information Technology Reference
In-Depth Information
Up until 20/12/2002, an ordinary agent
u
m
has the status
l
1
if
u
m
maintains
an account balance at least 1000 Euros. Conversely, up until 20/12/2002, if
u
m
makes a withdrawal that takes
u
m
's balance below 1000 Euros then the
downgrading act of withdrawal results in a status level transition from
l
1
to
l
2
.
After 20/12/2002, an ordinary agent
u
m
must maintain a balance of at least
1100 Euros for
u
m
to have the status
l
1
. Moreover, if
u
m
is an ordinary user
then
u
m
has the status
l
2
whenever
u
m
deposits a sum that terminates a period
of time during which
u
m
's account was overdrawn and
u
m
was assigned to
l
3
;
u
m
's assignment to
l
2
is terminated/
u
m
's assignment to
l
3
is initiated when
u
m
's
account becomes overdrawn. If
u
m
is a Gold-card holder then a different policy
applies, to wit: Gold-card holders have status
l
1
as long as they do not overdraw
by more than 100 Euros. If a Gold-card holder makes a withdrawal that results in
his or her account being overdrawn by more than 100 Euros then the withdrawal
induces a state transition from
l
1
to
l
2
. The policy relating to Gold-card holders
is not subject to any temporal constraint.
Suppose that the bank's policy is that, in the interval [01
/
12
/
2002
,
31
/
12
/
2002], users with an
l
2
status level may read any object other than
o
2
,
and that agents with a status level
l
1
can write object
o
1
up until 24/02/2002.
For that, the following
pla
clauses are included in
SBAC
(
ψ
):
pla
(
read, O, l
2
)
←
current time
(
T
)
,
01
/
12
/
2002
≤
T,T
≤
31
/
12
/
2002
,O
=
o
2
.
pla
(
write, o
1
,l
1
)
←
current time
(
T
)
,T <
24
/
02
/
2002
.
To represent the conditions on status level initiation and termination, an
APA would include the following
ECL
I
and
ECL
T
clauses in
SBAC
(
ψ
):
ECL
I
(
E,U,l
1
)
←
current time
(
T
)
, object
(
E,O
)
, ordinary
(
U
)
,
balance
(
O, X
)
,X
≥
1000
,T
≤
20
/
12
/
2002
.
ECL
T
(
E,U,l
1
)
←
current time
(
T
)
, object
(
E,O
)
, ordinary
(
U
)
,
balance
(
O, X
)
,X <
1000
,T
≤
20
/
12
/
2002
.
ECL
I
(
E,U,l
1
)
←
current time
(
T
)
, object
(
E,O
)
, ordinary
(
U
)
,
balance
(
O, X
)
,X
≥
1100
,T >
20
/
12
/
2002
.
ECL
T
(
E,U,l
1
)
←
current time
(
T
)
, object
(
E,O
)
, ordinary
(
U
)
,
balance
(
O, X
)
,X <
1100
,T >
20
/
12
/
2002
.
ECL
I
(
E,U,l
1
)
←
object
(
E,O
)
, goldcard
(
U
)
, balance
(
O, X
)
,X
≥−
100
.
ECL
T
(
E,U,l
1
)
←
object
(
E,O
)
, goldcard
(
U
)
, balance
(
O, X
)
,X <
−
100
.
ECL
I
(
E,U,l
2
)
←
object
(
E,O
)
, ordinary
(
U
)
, balance
(
O, X
)
,X
≥
0
.
ECL
T
(
E,U,l
2
)
← object
(
E,O
)
, ordinary
(
U
)
, balance
(
O, X
)
,X <
0
.
ECL
I
(
E,U,l
3
)
←
user
(
E,U
)
.
ECL
T
(
E,U,l
3
)
←
user
(
E,U
)
.