Formal Modeling and Verification of Context-Aware Systems using Event-B


Context awareness is a computing paradigm that makes applications responsive and adaptive with their environment. Formal modeling and verification of context-aware systems are challenging issues in the development as they are complex and uncertain. In this paper, we propose an approach to use a formal method Event-B to model and verify such systems. First, we specify a context aware system’s components such as context data entities, context rules, context relations by Event-B notions. In the next step, we use the Rodin platform to verify the system’s desired properties such as context constraint preservation. It aims to benefit from natural representation of context awareness concepts in Event-B and proof obligations generated by refinement mechanism to ensure the correctness of systems. We illustrate the use of our approach on a scenario of an Adaptive Cruise Control system.

Authors and Affiliations

Hong Anh Le, Ninh Thuan Truong


Related Articles

Context-aware Readings with Inbooki

E-books are more and more spreading among readers, who take advantage from the capability of reading them on different devices and of storing a whole library of books in a light and portable device. What is still missing...

Recommendation with quantitative implication rules

Association rules based recommendation is one of approaches to develop recommendation systems. However, such systems just focus on binary dataset, whereas many datasets are in the quantitative form. There are many soluti...

Internet of Thing Context Awareness Model

This paper aims to address key concept of context awareness in the Internet of Things (IoT) domain by providing a model that proactively monitors behaviour of devices and services. This concept represents context into tw...

Highlighted Activities of ICTCC 2016

The Second International Conference on Nature of Computation and Communication (ICTCC 2016) is jointly organized by EAI, Nguyen Tat Thanh University (NTTU), and Kien Giang University (KGU) and endorsed by the European Al...

Chronological states of viewer’s intentions using hidden Markov models and features of eye movement

To determine the possibility of predicting viewer’s internal states using the hidden Markov model, several features of eye movements were introduced to the model. Performance was measured using the data from a set of eye...

Download PDF file
  • EP ID EP45745
  • DOI
  • Views 243
  • Downloads 0

How To Cite

Hong Anh Le, Ninh Thuan Truong (2014). Formal Modeling and Verification of Context-Aware Systems using Event-B. EAI Endorsed Transactions on Context-aware Systems and Applications, 1(2), -.