Specifying a Reliable Broadcasting Protocol in Maude
This paper presents a formal and executable specification of a new
protocol for 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.
The protocol is specified in
rewriting logic. Rewriting
logic is a logic which extends algebraic
specification techniques
to concurrent and reactive systems. Among its possible advantages
over other executable
specification
formalisms are its being based upon a natural and well-known
formalism, its natural integration
of static and dynamic system aspects, the abstract modeling of
communication, and
its possibility to define execution strategies in
the
logic itself.
Rewriting logic seems particularly suitable for
specifying security and communication protocols. Such protocols are
complex enough to warrant prototyping and their operational nature
fits very well with rewriting logic.
Apart from presenting the final network protocol, this report also
aims at giving some snapshots of the specification effort of the group
illustrating how the rewriting logic language Maude
can be used in the
different stages of the specification and validation process. Due to
the complexity of the protocol, we first focussed on specifying the
protocol for the subcase of static networks, i.e., networks where no
channels or nodes are lost or created. The protocol for the dynamic
network setting was then developed, based of the final specification
for the static setting.