Information Technology Reference
During the execution of the service, the user is free to move into a different infostation,
to switch between devices or to do both.
A user cannot use the mLecture and mTest services simultaneously. The mTest service
should operate unaccompanied at all occasions.
This section presents the formalisation of the policies of the infostation-based context-aware
mLearning system using . We first introduce some naming conventions (sect. 6.2.1) which
are used in the specification of the system. Then we give the specification of two mServices
which are AAA and the mLecture services (sect. 6.3).
The following naming conventions are used to differentiate between variables' names and
constants. A variable name begins with a lowercase letter while a constant begins with a
number or a uppercase letter. The list of the constant names that are used in the
formalisation process is given in Table 4. And the list of variable names is given in
Table 4. Constants
6.3 A Model of the InfoStation-based mLearning system
The system consists mainly of one central ISC, multiple ISs and multiple user devices. Each
component of the system is modelled as an ambient. That is, the ISC, each IS and each user
device is modelled as an ambient. In particular, a device, PC say, being used by a user, 303
say, is modelled by an ambient named PC303 . The ISC ambient runs in parallel with the IS
ambients, and all the user devices within the range of an IS are child ambients of that IS