Specification and Analysis of a Reliable Broadcasting Protocol in Maude
The increasing importance, criticality, and complexity of
communications software makes very desirable the application of
formal methods to gain high assurance about its
correctness. These needs are even greater in the context of active
networks, because the difficulties involved in ensuring critical
properties such as security and safety for dynamically adaptive
software are substantially higher than for more static software
approaches.
There are many obstacles to the insertion of formal methods in this
area, and yet there is a real need to find adequate ways to increase
the quality and reliability of critical communication systems. The
present work reports on an ongoing case stufy 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 desigh. 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.
Indeed, the process of formally specifying the
protocol in Maude, and of symbolically executing and formally analysing the
resulting specification, has revealed many bugs and inconsistencies
very early in the design proecss, before much effort was put into the
implementation of the protocol.