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 409
- Downloads 0
Multivariate cube integrated retinal variable to visually represent multivariable data
For visualization of multivariable data, multivariate cube meets with the limitation of screen and human vision. Retinal variables are integrated into multivariate cube to enhance its visual characteristics. The selectiv...
Assistance to assessing rating students by language tuple- 4 scale
In this paper, we introduce an assistance to assessing rating the annual learning and process training of students in the opinion of experts, the approach of hedge algebra. It is advisary to make optimally fuzzy paramete...
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...
Book Titled Nature-Inspired Networking: Theory and Applications: An Introduction
Nature-Inspired Networking: Theory and Applications contains nine original, peer-reviewed chapters reporting on new developments of interest to the nature-inspired networking/computing communities. All chapters contain r...
Fast Radial and Bilateral Symmetry Detection Using Inverted Gradient Hash Maps
This paper presents a fast and novel algorithm for both radial and bilateral symmetry detection based on inverted gradient hash maps (IGHMs). A hash map is an associative array that stores image gradient magnitudes and o...