Publication Type

Journal Article

Version

publishedVersion

Publication Date

1-2014

Abstract

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.

Keywords

Model Check, Linear Temporal Logic, Liveness Property, Ambient Assist Live, Linear Temporal Logic Formula

Discipline

Software Engineering

Research Areas

Software and Cyber-Physical Systems

Publication

Lecture Notes in Artificial Intelligence

Volume

8780

First Page

62

Last Page

91

ISSN

0302-9743

Identifier

10.1007/978-3-662-44871-7_3

Publisher

Springer Verlag (Germany) / Springer Verlag (Germany): Computer Proceedings

Additional URL

https://doi.org/10.1007/978-3-662-44871-7_3

Download

Share

COinS