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...

Full description

Saved in:
Bibliographic Details
Main Authors: LIU, Yan, ZHANG, Xian, LIU, Yang, DONG, Jin Song, SUN, Jun, BISWAS, Jit, MOKHTARI, Mounir
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