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 413
- Downloads 0
Products, Coproducts and Universal Properties of Autonomic Systems
Self-* is widely considered as a foundation for autonomic computing. The notion of autonomic systems (ASs) and self-serves as a basis on which to build our intuition about category of ASs in general. In this paper we wil...
Clustering the objective interestingness measures based on tendency of variation in statistical implications
In recent years, the research cluster of objective interestingness measures has rapidly developed in order to assist users to choose the appropriate measure for their application. Researchers in this field mainly focus o...
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 Context-dependent Service Model
In service-oriented systems a service invariably is bound to a contract. This contract includes the functionalities and quality of services guarantees that the provider can make. But such guarantees are not absolute. A s...
Real Time Burning Image Classification Using Support Vector Machine
Burning image classification is critical and attempted problems in medical image processing. This paper has proposed the real time image classification for burning image to automatically identify the degrees of burns in...