[Home] [CV] [Publications]

Publications

Minus 1a5aa4f1c08b567c9107cba729de26bc87c17ab2b2f690eb45059193a1d6f587 Specifying a Reliable Broadcasting Protocol in Maude
Denker, G. and Garc\’ia-Luna-Aceves, J. J. and Meseguer, J. and \"Olveczky, P. C. and Raju, J. and Smith, B. and Talcott, C. L. - 1999

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.