Specification and Formal Analysis of a PLAN Algorithm in Maude
Bow-Yaw Wang*, Jose Meseguer**, and Carl A. Gunter*
* University of Pennsylvania, USA
** SRI International, USA
Abstract
Rewriting logic can be used as a semantic framework to model
next-generation networks and algorithms such as those of active
networks with greater flexibility than standard model checking
approaches. Using reflection, a wide range of formal analyses can be
performed on a given specification by specifying an analysis algorithm
as a metalevel theory that executes the specification as an
object-level entity. We illustrate how the reflective rewriting logic
language Maude can be used for this kind of formal specification and
analysis by means of an active network algorithm written in the PLAN
language, whose correct behavior from a given initial state is
formally analyzed using the proposed methods.
Keywords:
reflective rewriting logic, Maude, network algorithm, PLAN