Information Technology Reference
In-Depth Information
'nothing bad will happen'; and
liveness properties
, which assert that 'something good will
happen, eventually'. In the light of this classification, we wish to establish the liveness
property that every lecture request from a user is eventually replied to by the system,
provided that the user does not become infinitely unavailable after that request has been
made.
Theorem 7.1
Every user's lecture request will eventually get a reply, provided that the user stays
long enough in the system.
The proof of this theorem is based on the reduction semantics of given by a congruence
relation '
≡
' defined in Table 9 and a reduction relation '
→
' defined in Table 10.
In this proof we will assume, without loss of generality, that the user is using a laptop (PC)
to access the system from an infostation
. Given that the user is mobile, the following
cases must be considered:
1.
the user sends the request and waits for the reply in the same infostation
(i.e. the
user may move around within the range of the infostation)
2.
the user sends the request and move into a different infostation
,≠
.
In Case 1, the user behaviours can be modelled by the following ambient:
303[
∷〈001,303,,303〉.
∷(,).0]
(15)
This ambient sends a lecture request to the
ambient and waits for a reply from that
ambient, and then terminates. The lecture request contains the following information: (i) the
lecture ID,
Lect001
; (ii) the user ID,
303
; (iii) the device type,
PC
; and (iv) the name of the
ambient to reply to,
PC303
.
The behaviours of the
ambient is modelled by the process
in Eq. (5), which
basically receives a lecture request from a sibling ambient (e.g. a user device), forward the
request to the infostation
, get the reply from that infostation and forwards it to the very
ambient which initiated the request. How the infostation
interacts with the
ambient is specified in Eq. (8). These interactions between a user device, the
ambient and the infostation
can be expressed as a sequence of derivations using the
reduction relation
→
. Because of the space limit, we cannot give the full sequence of
derivations in this paper. For illustration, the following sequence of derivations describes
how a lecture request sent by the user gets to the infostation to be processed:
