A formal framework for context-aware systems specification and verification

Context-aware applications development is still a challenging issue due to their adaptive behavior complexity and uncertainty features. A conceptual framework, as an ideal reuse technique, is one of the most suitable solutions to simplify the development of such systems and overcome their development complexity. We aim in this paper to design a framework that promotes the ability to specify and verify context-aware systems to assist and facilitate designer's task. The objective is gained here by combining two complementary modeling techniques: Model-driven Engineering (MDE) and Formal Methods. Model-driven technique is adopted to design a modeling framework for context-aware systems. Nevertheless, this technique generally lacks formal semantics and it is unfit for model analysis. Therefore, we define a formal semantics to overcome these drawbacks. Moreover, we show how context-aware system's adaptive behavior can be verified according to their invariants by applying model-checking techniques.