Formal Specification of an Active Networks Programming Language

Mark-Oliver Stehr and Carolyn Talcott

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:

  1. Jose Meseguer, Peter Csaba Ölveczky, Mark-Oliver Stehr, and Carolyn L. Talcott. Maude as a wide-spectrum framework for formal modeling and analysis of active networks. In DARPA Active Networks Conference and Exposition (DANCE), San Francisco, May 2002, IEEE 2002. Available here.
  2. Mark-Oliver Stehr and Carolyn L. Talcott. Specifying an Active Network Programming Language in Rewriting Logic. Manuscript, SRI International and University of Hamburg, November 2001. A shorter version is available here.
  3. Mark-Oliver Stehr and Carolyn L. Talcott. Termination of Active Network Programs. Manuscript, SRI International and University of Hamburg, February 2002.
  4. Mark-Oliver Stehr and Carolyn Talcott: PLAN in Maude: Specifying an Active Network Programming Language , Fourth International Workshop on Rewriting Logic and its Applications (WRLA'2002), Pisa, Italy, September 19 - 21, 2000, Electronic Notes in Theoretical Computer Science 71, Elsevier, 2002 ( ENTCS Link )

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:

  1. README: instructions on how to run the examples
  2. plan-syntax.m: specification of the programming language syntax
  3. plan-sorts.m: various sorts (values, nonvalues, etc.) used in the specification
  4. plan-network.m: network related sorts/operations
  5. plan-semantics.m: operational semantics of the language
  6. p.m: loads the entire specification, i.e. all the files above
  7. topologies.m: definitions of two different network topologies
  8. semantics-runs.m: execution of various simple examples
  9. find-examples.m: definitions of two active network programs
  10. find-runs.m: execution of these programs on the above topologies