Network Protocol Simulation in Maude
by Carolyn Talcott and Ian Mason
Abstract:
On the one hand network and communication protocols are complex and
difficult to design, on the other hand it is important that network systems
are robust and reliable. Thus it is desirable to have formal models
augmented with tools that support simulation and testing that can be used by
designers of new protocols, both in the early stages of design, as well as
in later stages, where more rigorous formal analysis is important.
Rewriting logic and the language Maude (http://maude.csl.sri.com) with its
support of executable specifications and its ability to incorporate a wide
spectrum of formal methods using reflection is an ideal framework for
developing such tools.
In this talk we present the specification of a network model in Maude and describe some primitives for defining simulation strategies. The use of the model is illustrated with a simple HELLO sub-protocol taken from the IETF PIM-DM (Protocol Independent Multi-Cast-Dense Mode) RFC. The definition of strategies makes use of the reflective capability of Maude, and the real-time aspects such as timeout and timestamps are represented using ideas from the Real-Time Maude tool. The talk will begin with an introduction to rewriting logic, the Maude language with its support for distributed object-based computation.
The network model we present reflects the key aspects of the infra-structure on which typical communication protocols run. The network model is designed so that we may execute isolated protocols as well as develop techniques for composing sub-protocols to model the more complex protocols used in practice. The long term goal is to support simulation and formal analysis at many levels of detail and rigor.
Powerpoit Slides (generated from ppt)
Webviewable Slides (generated from ppt)
by Grit Denker, Jose Meseguer, and Carolyn Talcott
Abstract:
Communication between distributed objects may have to be protected against
random failures and malicious attacks; also, communication timeliness may be
essential or highly desired. Therefore, a distributed application often has
to be extended with communication services providing some kind of
fault-tolerance, secrecy, or quality-of-service guarantees. Ideally, such
services should be defined in a highly modular and dynamically composable
way, so that the combined assurance of several services can be achieved by
composition in certain cases, and so that services can be added or removed
from applications at runtime in response to changes in the environment. To
reason about the formal properties of such composable communication services
one first needs to give them a precise semantics. This paper proposes a
rewriting logic semantics for the so-called ``onion skin'' model of
distributed object reflection, in which different meta-objects,
providing different communication services, can be stacked on top of a basic
application object. Since the correct behavior of a service depends on the
type of hostile environment against which the service must protect
the application, rewriting logic should also be used to specify such hostile
environments. The service guarantees are then guarantees about the behavior
specified by the union of the rewrite theories specifying the basic
application, the services, and the hostile environment.
Web Viewable Slides (generated from ppt)
Specifying the Plan Language in Maude
by Carolyn Talcott (joint work with Mark-Oliver Stehr and Jose Meseguer)
Abstract:
Plan is a language being developed at UPenn for programming active networks.
Plan programs are sets of active packets that travel through a network
executing code specified nodes. The active nature of Plan programs makes it
important to have a formal specification of the semantics. The multiple
facets of Plan present several interesting specification challenges