Publication Type
Conference Proceeding Article
Version
acceptedVersion
Publication Date
7-2012
Abstract
Pervasive computing systems are heterogenous and complex as they usually involve human activities, various sensors and actuators as well as middleware for system controlling. Therefore, analyzing such systems is highly nontrivial. In this work, we propose to use formal methods for analyzing pervasive computing systems. Firstly, a formal modeling framework is proposed to cover the main characteristics of pervasive computing systems (e.g., context-awareness, concurrent communications, layered architectures). Secondly, we identify the safety requirements (e.g., free of deadlocks and conflicts etc.) and propose their specifications as safety and liveness properties. Finally, we demonstrate our ideas using a case study of a smart nursing home system. Experimental results show the effectiveness of our approach in exploring system behaviors and revealing system design flaws such as information inconsistency and conflicting reminder services.
Keywords
Pervasive Computing, Formal Modeling, System Verification
Discipline
Databases and Information Systems | Software Engineering
Research Areas
Software and Cyber-Physical Systems
Publication
Proceedings of the 17th IEEE International Conference on Engineering of Complex Computer Systems, ICECCS 2012, Washington, DC, July 18-20
First Page
1
Last Page
10
Identifier
10.1109/ICECCS20050.2012.6299212
Publisher
IEEE
City or Country
Washington, DC
Citation
1
Creative Commons License
This work is licensed under a Creative Commons Attribution-NonCommercial-No Derivative Works 4.0 International License.