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

Authors

DOI:

https://doi.org/10.4108/casa.1.2.e4

Keywords:

context awareness, refinement-based modeling, verification, Event-B

Abstract

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.

Downloads

Published

16-12-2014

How to Cite

1.
Anh Le H, Thuan Truong N. Formal Modeling and Verification of Context-Aware Systems using Event-B. EAI Endorsed Trans Context Aware Syst App [Internet]. 2014 Dec. 16 [cited 2024 Jun. 17];1(2):e4. Available from: https://publications.eai.eu/index.php/casa/article/view/2037

Funding data