Title :
Formal Analysis of Pervasive Computing Systems
Author :
Yan Liu ; Xian Zhang ; Jin Song Dong ; Yang Liu ; Jun Sun ; Biswas, J. ; Mokhtari, M.
Author_Institution :
Sch. of Comput., Nat. Univ. of Singapore, Singapore, Singapore
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 non-trivial. In this work, we propose to use formal methods for analyzing pervasive computing systems. Firstly, a formal modeling framework is proposed to cover main characteristics of pervasive computing systems (e.g., context-awareness, concurrent communications, layered architectures). Secondly, we identify the safety requirements (e.g., free of deadlock 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 :
formal specification; ubiquitous computing; actuators; concurrent communications; conflicting reminder services; context-awareness; formal modeling framework; human activities; information inconsistency; layered architectures; liveness properties; middleware; pervasive computing systems; safety properties; safety requirements; sensors; smart nursing home system; system behaviors; system design flaws; Adaptation models; Cognition; Computational modeling; Context; Pervasive computing; Sensor systems; Formal Modeling; Pervasive Computing; System Verification;
Conference_Titel :
Engineering of Complex Computer Systems (ICECCS), 2012 17th International Conference on
Conference_Location :
Paris
Print_ISBN :
978-1-4673-2156-3