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.
13.5.1 Action Systems
The action systems formalism is based on Dijkstra's language of guarded commands . This language includes assignment, sequential composition, conditional choice, and iteration.
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 S1 else S2 fi is the conditional ...