Formal Modeling and Verification of Context-Aware Systems using Event-B
Journal Title: EAI Endorsed Transactions on Context-aware Systems and Applications - Year 2014, Vol 1, Issue 2
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.
Authors and Affiliations
Hong Anh Le, Ninh Thuan Truong
Keywords
Related Articles
- EP ID EP45745
- DOI http://dx.doi.org/10.4108/casa.1.2.e4
- Views 351
- Downloads 0
The Approach of Applying Augmented Reality Application with Infographic for Supporting Health Care
There are more and more people can access the technology, digital divide has been reduced over the years. In this paper intend to clarify and demonstrated how Thailand want to apply the trendy and advance technology to p...
AndroCon: An Android-Based Context-Aware Middleware Framework
Mobile devices have become major sources of context-aware data due to their ubiquity and sensing capabilities. However, deploying mobile devices as dynamic, unabridged context data provider either locally or remotely is...
A Combination of Off-line and On-line Learning to Classifier Grids for Object Detection
We propose a new method for object detection by combining off-line and on-line boosting learning to classifier grids based on visual information without human intervention concerned to intelligent surveillance system. It...
A federation of simulations based on cellular automata in cyber-physical systems
In cyber-physical system (CPS), cooperation between a variety of computational and physical elements usually poses difficulties to current modelling and simulation tools. Although much research has proposed to address th...
A hybrid feature selection method for credit scoring
Reliable credit scoring models played a very important role of retail banks to evaluate credit applications and it has been widely studied. The main objective of this paper is to build a hybrid credit scoring model using...