[Home] [CV] [Publications]


Minus 1a5aa4f1c08b567c9107cba729de26bc87c17ab2b2f690eb45059193a1d6f587 PLAN in Maude: Specifying an Active Network Programming Language
Stehr, Mark-Oliver and Talcott, Carolyn - 2002

PLAN is a language designed for programming active networks, and can more generally be regarded as a model of mobile computation. PLAN generalizes the paradigm of imperative functional programming in an elegant way that allows for potentially recursive, remote function calls, and it provides a clear mechanism for the interaction between host and mobile code. Techniques for specifying and reasoning about such languages are of growing importance. In this paper we describe our specification of PLAN in Maude. We show how techniques for developing mathematical semantics of imperative functional programs (syntax-based semantics) and for formalizing variable binding constructs and mobile environments (CINNI calculus) are used in combination with the natural representation of concurrency and distribution provided by rewriting logic to develop a faithful model of the informal PLAN semantics. We also illustrate the wide-spectrum approach to formal modeling supported by Maude: executing PLAN programs; analyzing PLAN programs using search and model-checking; proving properties of particular PLAN programs; and proving general properties of the PLAN language. The ability to execute and analyze particular PLAN programs is useful for PLAN programmer, while analysis of the specification itself is important as a means of validating both the language design and the formal specification.