Formal Modeling and Verification of Context-Aware Systems using Event-B
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 form...
Main Authors: | , |
---|---|
Format: | Article |
Language: | English |
Published: |
European Alliance for Innovation (EAI)
2014-12-01
|
Series: | EAI Endorsed Transactions on Context-aware Systems and Applications |
Subjects: | |
Online Access: | http://eudl.eu/doi/10.4108/casa.1.2.e4 |
id |
doaj-5af77ccc567b4af1b046e0992ddb3d08 |
---|---|
record_format |
Article |
spelling |
doaj-5af77ccc567b4af1b046e0992ddb3d082020-11-24T21:47:55ZengEuropean Alliance for Innovation (EAI)EAI Endorsed Transactions on Context-aware Systems and Applications2409-00262014-12-011211010.4108/casa.1.2.e4Formal Modeling and Verification of Context-Aware Systems using Event-BHong Anh Le0Ninh Thuan Truong1Hanoi University of Mining and Geology, Duc Thang, Bac Tu Liem, Ha Noi, Viet Nam; lehonganh@humg.edu.vnVNU - University of Engineering and Technology, 144 Xuan Thuy, Cau Giay, Ha Noi, Viet NamContext 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.http://eudl.eu/doi/10.4108/casa.1.2.e4ontext awarenessrefinement-based modelingverificationEvent-B |
collection |
DOAJ |
language |
English |
format |
Article |
sources |
DOAJ |
author |
Hong Anh Le Ninh Thuan Truong |
spellingShingle |
Hong Anh Le Ninh Thuan Truong Formal Modeling and Verification of Context-Aware Systems using Event-B EAI Endorsed Transactions on Context-aware Systems and Applications ontext awareness refinement-based modeling verification Event-B |
author_facet |
Hong Anh Le Ninh Thuan Truong |
author_sort |
Hong Anh Le |
title |
Formal Modeling and Verification of Context-Aware Systems using Event-B |
title_short |
Formal Modeling and Verification of Context-Aware Systems using Event-B |
title_full |
Formal Modeling and Verification of Context-Aware Systems using Event-B |
title_fullStr |
Formal Modeling and Verification of Context-Aware Systems using Event-B |
title_full_unstemmed |
Formal Modeling and Verification of Context-Aware Systems using Event-B |
title_sort |
formal modeling and verification of context-aware systems using event-b |
publisher |
European Alliance for Innovation (EAI) |
series |
EAI Endorsed Transactions on Context-aware Systems and Applications |
issn |
2409-0026 |
publishDate |
2014-12-01 |
description |
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. |
topic |
ontext awareness refinement-based modeling verification Event-B |
url |
http://eudl.eu/doi/10.4108/casa.1.2.e4 |
work_keys_str_mv |
AT honganhle formalmodelingandverificationofcontextawaresystemsusingeventb AT ninhthuantruong formalmodelingandverificationofcontextawaresystemsusingeventb |
_version_ |
1725894629678645248 |