Copyright © 2008 The Institute of Electronics, Information and Communication Engineers
Special Section on Knowledge-Based Software Engineering -- Papers -- Ubiquitous Computing |
Query Language for Location-Based Services: A Model Checking Approach
1 The author is with the Graduate School for Advanced Studies, National Institute of Informatics, Kanagawa-ken, 240–0193 Japan., 2 The authors are with National Institute of Informatics, Tokyo, 101–8430 Japan. E-mail: hoareau{at}nii.ac.jp
We present a model checking approach to the rationale, implementation, and applications of a query language for location-based services. Such query mechanisms are necessary so that users, objects, and/or services can effectively benefit from the location-awareness of their surrounding environment. The underlying data model is founded on a symbolic model of space organized in a tree structure. Once extended to a semantic model for modal logic, we regard location query processing as a model checking problem, and thus define location queries as hybrid logic-based formulas. Our approach is unique to existing research because it explores the connection between location models and query processing in ubiquitous computing systems, relies on a sound theoretical basis, and provides modal logic-based query mechanisms for expressive searches over a decentralized data structure. A prototype implementation is also presented and will be discussed.
Key Words: ubiquitous computing, location-based services, query language, model checking
Manuscript received July 12, 2007. Manuscript revised October 17, 2007.
Reference
[1] L. de Alfaro, "Model checking the World Wide Web," Proc. 13th International Conf. on Computer Aided Verification (CAV'01), pp.337–349, Springer-Verlag, 2001. [2] L. Afanasiev, M. Franceschet, M. Marx, and M. de Rijke, "CTL model checking for processing simple XPath queries," Proc. 11th International Symposium on Temporal Representation and Reasoning (TIME'04), pp.117–124, IEEE Computer Society, 2004. [3] C. Areces and B. ten Cate, "Hybrid logics," in Handbook of Modal Logic, ed. P. Blackburn, F. Wolter, and J. van Benthem, Elsevier2005. [4] M. Bauer, C. Becker, and K. Rothermel, "Location models from the perspective of context-aware applications and mobile ad hoc networks," Personal and Ubiquitous Computing, vol.6, no.5-6, pp.322–328, Springer-Verlag, 2002. [5] C. Becker and F. Dürr, "On location models for ubiquitous computing," Personal and Ubiquitous Computing, vol.9, no.1, pp.20–31, Springer-Verlag, 2005. [6] M. Beigl, T. Zimmer, and C. Decker, "A location model for communicating and processing of context," Personal and Ubiquitous Computing, vol.6, no.5–6, pp.341–357, Springer-Verlag, 2002. [7] E.M. Clarke and B.H. Schlingloff, "Model checking," in Handbook of automated reasoning, pp.1635–1790, ed. J.A. Robinson and A. Voronkov, Elsevier Science Publishers B.V., 2001. [8] M. Franceschet, A. Montanari, and M. de Rijke, "Model checking for combined logics with an application to mobile systems," Automated Software Engineering, vol.11, no.3, pp.289–321, Kluwer Academic Publishers, 2004. [9] R.H. G>üting and M. Schneider, Moving Objects Databases, Morgan Kaufmann Publishers, 2005. [10] J. Hightower, "From position to place," Proc. 2003 Workshop on Location-Aware Computing, pp.10–12, Oct. 2003. [11] F. Hohl, U. Kubach, A. Leonhardi, K. Rothermel, and M. Schwehm, "Next century challenges: Nexus–an open global infrastructure for spatial-aware applications," Proc. 5th Annual ACM/IEEE International Conf. on Mobile Computing and Networking (MOBICOM'99), pp.249–255, ACM Press, 1999. [12] U. Leonhardt, Supporting Location-Awareness in Open Distributed Systems, Ph.D. Thesis, Department of Computing, Imperial College, London, 1998. [13] G. Lowe, "Breaking and fixing the Needham-Schroeder public-key protocol using FDR," Proc. 2nd International Workshop on Tools and Algorithms for Construction and Analysis of Systems (TACAS'96), pp.147–166, Springer-Verlag, 1996. [14] M. Negri, G. Pelagatti, and L. Sbattella, "Formal semantics of SQL queries," ACM Trans. Database Syst., vol.16, no.3, pp.513–534, 1991. [15] I. Satoh, "A location model for pervasive computing environments," Proc. 3rd IEEE International Conf. on Pervasive Computing and Communications (PERCOM'05), pp.215–224, IEEE Computer Society, 2005. [16] W. Visser, K. Havelund, G. Brat, and S. Park, "Model checking programs," Proc. 15th IEEE International Conf. on Automated Software Engineering (ASE'00), p.3, IEEE Computer Society, 2000. [17] O. Wolfson, S. Chamberlain, K. Kalpakis, and Y. Yesha, "Modeling moving objects for location based services," Proc. US NSF Workshop on Developing an Infrastructure for Mobile and Wireless Systems, pp.46–58, Springer-Verlag, 2001.
CiteULike 
Connotea 
Del.icio.us What's this?
This Article 
Abstract
Full Text (PDF)
Alert me when this article is cited
Alert me if a correction is posted
Services
Email this article to a friend
Similar articles in this journal
Alert me to new issues of the journal
Add to My Personal Archive
Download to citation manager
Request Permissions
Google Scholar
Articles by HOAREAU, C.
Articles by SATOH, I.
Social Bookmarking
What's this?