Intelligent Distributed eLearning Architecture - Intelligent Systems - page 214

after that ID. The behaviour of a lecture ambient is specified in Eq. (7). The Lectures ambient
behaves exactly as the cache ambient specified in Eq. (6).

Infostation centre We now formalise the behaviour of the ISC when it receives a request
from an IS. We are interested in two types of request in this paper: an AAA request and a
lecture request.

When the ISC receives an AAA request from an IS, it updates the user's account with its new
location and then replies to that IS with an acknowledge along with a list of available
services. For the sake of simplicity, the service list is represented by the name 'SLIST' . This is
modelled by the following process:

! ∷(,,,).↓〈 〉.↓().

(13)

∷〈,,〉.0
After receiving a lecture request, the ISC checks whether the user requesting the service is
currently taking a mTest. This is done by it sending a message to the corresponding user's
account ambient. That user's account ambient reply with 0 for 'No' and 1 for 'Yes'. If the
reply is 'Yes' then the ISC fetches the current location of the user and forward a 'DENIED'
message to that location. If the reply is 'No' and the flag is set to 1, a 'OK' message is
forwarded to the current user location; otherwise (i.e. reply is 'No' and the flag is set to 0),
the ISC fetches the appropriate lecture version for the user device and sends it to the current
user location. This behaviour is represented by the following process:

! ∷ ( ,,,, ) .↓ 〈 〉 .↓ ( ) . )

(14)

where

≙ ( =1 ) ?↓ 〈 〉 .↓ ( ) .∷ 〈 ,, 〉 .0

and

So the whole behaviour of the ISC is modelled by the following process:

≙.(13)|.(14)

7. Validation

Now that a formal model of the infostation-based mLearning system has been presented, we
show how this model can be used to validate the properties of the mLearning system.
Lamport proposed two main classes of system's properties: safety properties , which state that