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 in fact 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. As a consequence, in spite of the existence of good research contributions in formal approaches to areas such as distributed algorithms and cryptographic protocols, in practice new systems are developed for the most part in a traditional engineering way, using informal techniques, and without much to go by before detailed simulations or an actual implementation except for pseudocode and informal specifications. 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 specifications, 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.