Please use this identifier to cite or link to this item: http://hdl.handle.net/10397/10786
Title: Formal specification and runtime detection of temporal properties for asynchronous context
Authors: Wei, H
Huang, Y
Cao, J 
Ma, X
Lu, J
Keywords: 3-valued semantics
Branching time
Contextual property
Issue Date: 2012
Source: 2012 IEEE International Conference on Pervasive Computing and Communications, PerCom 2012, 2012, 6199846, p. 30-38 How to cite?
Abstract: Formal specification and runtime detection of temporal properties for pervasive context is one of the primary approaches to achieving context-awareness. Though temporal logics have been widely used in specification of temporal properties, they are faced with severe challenges in Pervasive Computing (PvC) scenarios. First, temporal logics are traditionally defined over infinite traces of possible system behavior. However in PvC scenarios, applications observe finite prefixes of (potentially infinite) traces of environment state evolution, and adapt their behavior accordingly. Second, specification and detection of temporal properties are challenged by the intrinsic asynchrony of PvC environments. Discussions above necessitate a systematic approach to formal specification and runtime detection of temporal properties for asynchronous context. To this end, we propose CTL 3 (3-valued Computation Tree Logic), which i) adopts 3-valued semantics to capture the inconclusiveness when applications only observe finite prefixes of environment state evolution; ii) inherits the notion of branching time to capture the uncertainty resulting from the asynchrony of PvC environments. A case study is conducted to demonstrate how CTL 3 supports context-awareness in PvC scenarios. The runtime checking algorithm of CTL 3 is implemented and evaluated over MIPA-the open-source context-aware middle-ware we developed. The case study demonstrates the necessity of adopting CTL 3 in PvC scenarios, while the performance measurements show the cost-effectiveness of runtime checking contextual properties in CTL 3.
Description: 10th IEEE International Conference on Pervasive Computing and Communications, PerCom 2012, Lugano, 19-23 March 2012
URI: http://hdl.handle.net/10397/10786
ISBN: 9781467302586
DOI: 10.1109/PerCom.2012.6199846
Appears in Collections:Conference Paper

Access
View full-text via PolyU eLinks SFX Query
Show full item record

SCOPUSTM   
Citations

8
Last Week
0
Last month
0
Citations as of Oct 9, 2017

Page view(s)

41
Last Week
1
Last month
Checked on Oct 15, 2017

Google ScholarTM

Check

Altmetric



Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.