Formal specification and runtime detection of temporal properties for asynchronous context

Hengfeng Wei, Yu Huang, Jiannong Cao, Xiaoxing Ma, Jian Lu

Research output: Chapter in book / Conference proceedingConference article published in proceeding or bookAcademic researchpeer-review

10 Citations (Scopus)

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 CTL3(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 CTL3supports context-awareness in PvC scenarios. The runtime checking algorithm of CTL3is implemented and evaluated over MIPA-the open-source context-aware middle-ware we developed. The case study demonstrates the necessity of adopting CTL3in PvC scenarios, while the performance measurements show the cost-effectiveness of runtime checking contextual properties in CTL3.
Original languageEnglish
Title of host publication2012 IEEE International Conference on Pervasive Computing and Communications, PerCom 2012
Pages30-38
Number of pages9
DOIs
Publication statusPublished - 4 Jun 2012
Event10th IEEE International Conference on Pervasive Computing and Communications, PerCom 2012 - Lugano, Switzerland
Duration: 19 Mar 201223 Mar 2012

Conference

Conference10th IEEE International Conference on Pervasive Computing and Communications, PerCom 2012
CountrySwitzerland
CityLugano
Period19/03/1223/03/12

Keywords

  • 3-valued semantics
  • branching time
  • contextual property

ASJC Scopus subject areas

  • Computer Networks and Communications

Cite this