Formalising policies of a mLearning system using CCA
Mohammed Al-Sammarraie, François Siewe, Hussein Zedan · 2010
The Calculus of Context-aware Ambients (CCA in short) has been proposed as a suitable notation for modelling mobile applications that are context-aware. This paper considers a real-world case study of an infostation-based mLearning system which enables mobile devices such as cellular phones, laptops and personal digital assistants to communicate to each other and to access a number of mlearning services within a university campus. Such a dynamic system must enforce complex policies to cope with mobility and context-awareness. We show how these policies can be formalised and verified using CCA. In particular an important liveness property of the mLearning system is proved using the reduction semantics of CCA.