Provably correct pervasive computing environments

Anand Ranganathan, R H Campbell

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract

The field of pervasive computing has seen a lot of exciting innovations in the past few years. However, there are currently no mechanisms for describing the properties and capabilities of pervasive computing environments in a formal manner. This makes it difficult to prove the correctnesss of a pervasive computing environment, i.e. to verify that the environment satisfies certain desired properties. In this paper, we propose a formal model for describing pervasive computing environments based on ambient calculus and the associated ambient logic. The model allows us to state and verify several properties of these environments such as "anywhere anyhow services", "mobility of devices and applications" and "context-aware adaptation". The model allows us to describe the resources present in an environment, the operations that can be performed in the environment, and how users can use the resources in th environment to perform different kinds of activities. As a case study, we shall describe some of the resources and operations supported by the Gaia middleware using this model, and verify an example property of a pervasive computing environment supported by Gaia.

Original languageEnglish (US)
Title of host publication6th Annual IEEE International Conference on Pervasive Computing and Communications, PerCom 2008
Pages160-169
Number of pages10
DOIs
StatePublished - Aug 15 2008
Event6th Annual IEEE International Conference on Pervasive Computing and Communications, PerCom 2008 - Hong Kong, Hong Kong
Duration: Mar 17 2008Mar 21 2008

Publication series

Name6th Annual IEEE International Conference on Pervasive Computing and Communications, PerCom 2008

Other

Other6th Annual IEEE International Conference on Pervasive Computing and Communications, PerCom 2008
CountryHong Kong
CityHong Kong
Period3/17/083/21/08

ASJC Scopus subject areas

  • Computer Networks and Communications
  • Communication

Fingerprint Dive into the research topics of 'Provably correct pervasive computing environments'. Together they form a unique fingerprint.

Cite this