Formal specification and runtime detection of temporal properties for asynchronous context

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-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₃ supports context-awareness in PvC scenarios. The runtime checking algorithm of CTL₃ is implemented and evaluated over MIPA - the open-source context-aware middle-ware we developed. The case study demonstrates the necessity of adopting CTL₃ in PvC scenarios, while the performance measurements show the cost-effectiveness of runtime checking contextual properties in CTL₃.