Mobile Intelligence

13.5 FORMALIZING CONTEXT AWARENESS AND CONTEXT DEPENDENCY

We start by giving a brief overview of the action system formalism and then present how we model context awareness and context dependency within this formalism. By mapping the formal model back to the software architecture of wireless sensor networks, we show some realistic implementations of this model on system software research.

Figure 13.1 The sensornet system framework.

13.5.1 Action Systems

The action systems formalism is based on Dijkstra's language of guarded commands [14]. This language includes assignment, sequential composition, conditional choice, and iteration.

13.5.1.1 Actions

An action is a guarded command, that is, a construct of the form g → S, where g is a predicate, the guard, and S is a program statement, the body. An action is said to be enabled when its guard is evaluated to true. If an action does not change the program state, it is called a stuttering action.

The body S of an action is defined as follows:

Here x is a list of attributes, e is a corresponding list of expressions, x′ is a list of variables standing for unknown values, and R is a relation specified in terms of x and x′. Intuitively, skip is an stuttering action, x := e is a multiple assignment, if g then S₁ else S₂ f_i is the conditional ...