Towards formal modelling and verification of pervasive computing systems
Smart systems equipped with emerging pervasive computing technologies enable people with limitations to live in their homes independently. However, lack of guarantees for correctness prevent such system to be widely used. Analysing the system with regard to correctness requirements is a challenging...
Saved in:
Main Authors: | , , , , , , |
---|---|
Format: | text |
Language: | English |
Published: |
Institutional Knowledge at Singapore Management University
2014
|
Subjects: | |
Online Access: | https://ink.library.smu.edu.sg/sis_research/4981 https://ink.library.smu.edu.sg/context/sis_research/article/5984/viewcontent/10.1007_978_3_662_44871_7.pdf |
Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
Institution: | Singapore Management University |
Language: | English |
id |
sg-smu-ink.sis_research-5984 |
---|---|
record_format |
dspace |
spelling |
sg-smu-ink.sis_research-59842020-03-12T07:37:57Z Towards formal modelling and verification of pervasive computing systems LIU, Yan ZHANG, Xian LIU, Yang DONG, Jin Song SUN, Jun BISWAS, Jit MOKHTARI, Mounir Smart systems equipped with emerging pervasive computing technologies enable people with limitations to live in their homes independently. However, lack of guarantees for correctness prevent such system to be widely used. Analysing the system with regard to correctness requirements is a challenging task due to the complexity of the system and its various unpredictable faults. In this work, we propose to use formal methods to analyse pervasive computing (PvC) systems. Firstly, a formal modelling framework is proposed to cover the main characteristics of such systems (e.g., context-awareness, concurrent communications, layered architectures). Secondly, we identify the safety requirements (e.g., free of deadlocks and conflicts) and specify them as safety and liveness properties. Furthermore, based on the modelling framework, we propose an approach of verifying reasoning rules which are used in the middleware for perceiving the environment and making adaptation decisions. Finally, we demonstrate our ideas using a case study of a smart healthcare system. Experimental results show the usefulness of our approach in exploring system behaviours and revealing system design flaws such as information inconsistency and conflicting reminder services. 2014-01-02T08:00:00Z text application/pdf https://ink.library.smu.edu.sg/sis_research/4981 info:doi/10.1007/978-3-662-44871-7_3 https://ink.library.smu.edu.sg/context/sis_research/article/5984/viewcontent/10.1007_978_3_662_44871_7.pdf http://creativecommons.org/licenses/by-nc-nd/4.0/ Research Collection School Of Computing and Information Systems eng Institutional Knowledge at Singapore Management University Model Check Linear Temporal Logic Liveness Property Ambient Assist Live Linear Temporal Logic Formula Software Engineering |
institution |
Singapore Management University |
building |
SMU Libraries |
continent |
Asia |
country |
Singapore Singapore |
content_provider |
SMU Libraries |
collection |
InK@SMU |
language |
English |
topic |
Model Check Linear Temporal Logic Liveness Property Ambient Assist Live Linear Temporal Logic Formula Software Engineering |
spellingShingle |
Model Check Linear Temporal Logic Liveness Property Ambient Assist Live Linear Temporal Logic Formula Software Engineering LIU, Yan ZHANG, Xian LIU, Yang DONG, Jin Song SUN, Jun BISWAS, Jit MOKHTARI, Mounir Towards formal modelling and verification of pervasive computing systems |
description |
Smart systems equipped with emerging pervasive computing technologies enable people with limitations to live in their homes independently. However, lack of guarantees for correctness prevent such system to be widely used. Analysing the system with regard to correctness requirements is a challenging task due to the complexity of the system and its various unpredictable faults. In this work, we propose to use formal methods to analyse pervasive computing (PvC) systems. Firstly, a formal modelling framework is proposed to cover the main characteristics of such systems (e.g., context-awareness, concurrent communications, layered architectures). Secondly, we identify the safety requirements (e.g., free of deadlocks and conflicts) and specify them as safety and liveness properties. Furthermore, based on the modelling framework, we propose an approach of verifying reasoning rules which are used in the middleware for perceiving the environment and making adaptation decisions. Finally, we demonstrate our ideas using a case study of a smart healthcare system. Experimental results show the usefulness of our approach in exploring system behaviours and revealing system design flaws such as information inconsistency and conflicting reminder services. |
format |
text |
author |
LIU, Yan ZHANG, Xian LIU, Yang DONG, Jin Song SUN, Jun BISWAS, Jit MOKHTARI, Mounir |
author_facet |
LIU, Yan ZHANG, Xian LIU, Yang DONG, Jin Song SUN, Jun BISWAS, Jit MOKHTARI, Mounir |
author_sort |
LIU, Yan |
title |
Towards formal modelling and verification of pervasive computing systems |
title_short |
Towards formal modelling and verification of pervasive computing systems |
title_full |
Towards formal modelling and verification of pervasive computing systems |
title_fullStr |
Towards formal modelling and verification of pervasive computing systems |
title_full_unstemmed |
Towards formal modelling and verification of pervasive computing systems |
title_sort |
towards formal modelling and verification of pervasive computing systems |
publisher |
Institutional Knowledge at Singapore Management University |
publishDate |
2014 |
url |
https://ink.library.smu.edu.sg/sis_research/4981 https://ink.library.smu.edu.sg/context/sis_research/article/5984/viewcontent/10.1007_978_3_662_44871_7.pdf |
_version_ |
1770575166045159424 |