From Model Checking to Data Management in Pervasive Computing: A Location-based Query-processing Framework

This paper presents a query-processing framework for location-based services. The proposed approach aims at complementing existing context-aware services wherein locations of people, physical objects and services arc modeled in a symbolic manner, independently of any sensing technology. To deliver contextual information to the various components of a pervasive computing platform, current systems tend to query the underlying location models in an ad-hoc manner. This makes it difficult to guarantee the quality of the results, and hence the reliability of context-aware services. The main idea behind our framework is to apply and adapt the principles of model checking to query the contextual data structures. Because such query mechanisms have to be sound, our approach is build upon a logic-based query language. We therefore ensure that the results of any query (i) do not miss any information that satisfy its necessary and sufficient conditions and (ii) do not contain any information that does not satisfy the conditions. We describe the implementation of or framework and discuss its applicability to existing graph-based location models.