Keywords: Active Networks, PLAN, Switchware, Formal Specification
Active networks are networks with nodes that do not operate according to a fixed scheme (e.g. as conventional routers) but are instead fully programmable and provide execution environments for programs that can be received from other nodes via the network. An active network does not necessarily have a static topology, so that also unreliable, wireless and hybrid networks are subsumed by this notion. The development of suitable programming paradigms for active network applications is an important research objective.
A particularly interesting paradigm is supported by the active network programming language PLAN, which has been developped and implemented by the group of Carl A. Gunter at the University of Pennsylvania. On an abstract level, PLAN can be regarded as language with built-in support for mobility. It is based on a functional programming language with a concept of location and remote function invocation, which is quite different from the remote procedure calls known from conventional languages. Remote function invocations are asynchronous, and they can be recursive and typically coincide with a change of location, which is realized by the emission of packets containing chunks, i.e. programs as data. Furthermore, PLAN allows programming with side effects and services which can be location dependent. Another aspect is resource awareness which ensures that all PLAN programs are terminating.
Our contribution is a specification of PLAN, and in fact of a more general language, using rewriting logic as a formal specification language. The formal specification is executable and therefore provides an execution environment of PLAN programs. The specification uses an abstract reduction machine based on a technique inspired by Felleisen, which provides a more high-level view than the standard SECD approach. The specification also benefits from the use of CINNI, a new calculus of names and substitutions, which make the issues of bindings and environments precise, without going into implementation details. There are other interesting aspects such as multi-level concurrency and locality of information that are nicely captured by multiset rewriting in rewriting logic. In summary, the high-level nature of our specification provides not only a suitable level for abstract execution, but more importantly for mathematical reasoning and formal theorem proving. On the other hand, the formal specification is intuitive, easy to understand and can serve as a useful guide for application programmers and language implementors.
Relevant References:
References concerned with the PLAN language and its implementation
can be found here.
Information about the relation between PLAN and the more restricted SNAP
language can be found here.
Our specification of PLAN was part of the DARPA project Maude: A Wide-Spectrum Formal Language for Secure Active Networks.
The Formal Specification in Maude 2.0 (available
here) can be found
here.
This package contains the
following files: