Location-Awareness with Action Systems

Introduction

Our lifestyles are more dynamic by the year (Tanenbaum, 2003): we talk on the mobile phone while on the go; we can work on our wirelessly connected laptops mostly everywhere in the big cities, and we can attach network chips and wireless sensors to basically everything around us, thus making the environment aware of our requests and needs (Culler, Estrin, & Srivastava, 2004). While there are important issues related to these opportunities, such as economical, ethical, social, and environmental implications (Bohn, Coroama, Langheinrich, Mattern, & Rohs, 2005), they also opened a wide range of applications (Romer & Mattern, 2004) that can make people much more efficient, in control, and almost all the time connected.

The technologies supporting this dynamic way of computing and communicating are continuously developing and becoming more complex. In order to be confident in the flexibility introduced by mobile phones, laptops, and wireless networks and sensors, we need to ensure that they work dependably. Dependability refers to the degree of reliance that can be placed on these devices and infrastructures (Laprie, 1985; Laprie, Avizienis, & Kopetz, 1992; RODIN) and encompasses characteristics of a system such as security, that is the non-occurrence of unauthorized disclosure of information; integrity, that is the non-occurrence of inadequate information alteration; availability, that is the readiness for correct service of the system; reliability, that is the property of the system to continuously provide service.

In order to analyze whether a system is dependable, we need to have a model for it. One feature that is characteristic of models for mobile phones, laptops, wireless sensors, and networks is that of location. Mobility implies a starting and an ending point. Wireless sensors provide, for instance, data about the environment or habitats (Klimat; Teymorian, Ma, & Lu, 2009) whose location is the most important aspect. The wireless devices are working as long as they are in range, i.e., another location-based concept. Hence, all these devices and infrastructures take location into account and their functioning adjusts accordingly to the values of their locations.

One way to ensure dependability is provided by mathematically-based modeling, analysis, and development of the location-aware systems. These techniques are known as formal methods. The approach implies the capture of system requirements in a specific, precise format, which is a formal model that can be analyzed for various properties and, if the formal method permits, also stepwise developed until an implementation is formed. By following such a formal development, we are sure that the final result implements the requirements of the system. In this chapter we present the approach to location-awareness provided by the action systems formal method.

Action systems were introduced for modeling and analyzing distributed systems (Back & Kurki-Suonio, 1983). The main idea is that the system state, given by variable values, is non-deterministically evaluated and modified by atomic guarded statements called actions. An action system is a finite collection of state variables and actions. The state and the actions in an action system can be interpreted as distributed over a network, however, their distribution has traditionally been location-transparent. This is enough for modeling computations in local area networks where there is no significant mobility. For modeling dynamic and mobile computations that are aware of their surrounding contexts (Neovius, Sere, Yan, & Satpathy, 2006) locations were introduced to action systems (Petre, Sere, & Waldén, 1999).

Variables, actions, and action systems are thus considered network resources and, by definition, each has a location in the supporting network. While the locations of variables (data resources) and actions (code resources) are independent, the location of an action system is defined as a function of the locations of its component variables and actions. Several replicas of a resource can be defined at distinct locations in the network. Movement is defined as the update of the resource's location; if that resource is replicated, then only one copy changes its location, while the others stay put.