| Overview |
The present work reports on an ongoing case study in which a new reliable broadcasting protocol (RBP) currently under development at the University of California at Santa Cruz (UCSC) has been formally specified and analyzed, leading to many corrections and improvements to the original design. Indeed, the process of formally specifying the protocol, and of symbolically executing and formally analyzing the resulting specification, has revealed many bugs and inconsistencies very early in the design process, before the protocol was implemented.
RBP performs reliable broadcasting of information in networks with dynamic topology. Reliable broadcasting is not trivial when the topology of the network can change due to failure and mobility. The aim is to ensure that all nodes that satisfy certain connectedness criteria receive the information within finite time, and that the source is notified about it. The protocol should furthermore incur as low latency and as few messages as possible.
A message-passing object-oriented approach seems particularly natural
for communication protocols and can be naturally formalized in rewriting
logic. Using the rewriting logic-based Maude interpreter,
we can prototype and debug the RBP protocol specification. But since a
protocol can have many different behaviors, to properly analyze the system
it becomes important to explore not just the single execution provided
by some default strategy, but many other executions. For this purpose we
defined a search strategy that explores all executions
of a system for a given initial configuration.
The amount of effort required in the formal specification and analysis
process has been moderate, and it has been relatively easy for the
researchers at UCSC to learn and use the specification formalism
involved, so that the formal specification task has indeed been
carried out in a joint way by researchers at SRI International,
Stanford, and UCSC.
| Maude Specifications and Samples |
| Papers |
| [Maude Home Page] |