Provably correct pervasive computing environments

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.