Design and Validation of a Context-Aware Publish-Subscribe Model

Abstract

A system is said to be context-aware if it can extract, interpret and use contextual information to adapt its functionality and enhance its utility. Context awareness allows the application to gain sensitivity for many environmental parameters that are beyond the reach of conventional systems. Human factors related to context include information about the user (knowledge of habits, emotional state), the user’s social environment (co-location of others, social interaction, group dynamics), and the user’s tasks (spontaneous activity, engaged tasks, general goals). With access to this contextual information, there are many exciting possibilities for applications involving direct human interaction.

Software modelling is one of the first steps in the life cycle of a software system. Software models can lead to the discovery of errors in a system, which is useful as the early discovery of such flaws can enable the designers to update the inexpensive system model. By not using system models before the development of the full scale system, we risk the discovery of major problems later on in the life cycle, which will be more expensive to fix.

Validation of any software system is an essential part of the development life cycle. The validation of context-aware systems is especially challenging as the input range of the system is loosely defined. But despite this it is very important to validate context-aware systems thoroughly because it is possible that a subset of possible inputs to the system can be part of a failure-critical user interaction. Modeling and validation are important activities in the development or enhancement of all software systems. While software modelling helps check the properties of the systems before actual development, software validation is essential for ensuring the quality of the software based on the original software requirements.

This thesis focuses on the modeling and the validation of formal case study design models for context-aware systems based on the event based and publish-subscribe pattern. The study validates formal case study design models against relevant properties using a model checker.