Formal Specification of a Context-aware Whiteboard System in CCA

A context-aware whiteboard system provides a number of services in a smart classroom including registering students as they enter the classroom; logging students and lecturers in to the blackboard virtual learning environment at the beginning of each lecture and logging them out at the end of the lecture. This system also notifies students of their absence to a lecture and maintains a list of attendance automatically. Using information from the timetable, it is aware of the lectures that are scheduled to take place in the classroom and the students that are allowed to attend these lectures. Finally, it allows students and lecturers to interact with teaching materials such as lecture slides and videos stored in the blackboard virtual learning environment. This paper proposes a formal specification of the white board system in the Calculus of Context-aware Ambients (CCA in short). This enables the formal analysis of the white board system using the execution environment of CCA. Some important properties of a classroom white board system have been validated as a proof of concept.