Research Article
Formal Modeling and Verification of Context-Aware Systems using Event-B
@ARTICLE{10.4108/casa.1.2.e4, author={Hong Anh Le and Ninh Thuan Truong}, title={Formal Modeling and Verification of Context-Aware Systems using Event-B}, journal={EAI Endorsed Transactions on Context-aware Systems and Applications}, volume={1}, number={2}, publisher={ICST}, journal_a={CASA}, year={2014}, month={12}, keywords={context awareness, refinement-based modeling, verification, Event-B}, doi={10.4108/casa.1.2.e4} }- Hong Anh Le
Ninh Thuan Truong
Year: 2014
Formal Modeling and Verification of Context-Aware Systems using Event-B
CASA
ICST
DOI: 10.4108/casa.1.2.e4
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.
Copyright © 2014 Hong Anh Le and Ninh Thuan Truong, licensed to ICST. This is an open access article distributed under the terms of the Creative Commons Attribution license (http://creativecommons.org/licenses/by/3.0/), which permits unlimited use, distribution and reproduction in any medium so long as the original work is properly cited.
