Validation of distributed algorithms and protocols

摘要

The use of formal description techniques allows the partial automation of the design, the validation, and the implementation of communication protocols and distributed algorithms. In this paper, we present a methodology for validation of distributed algorithms and protocols, and our experiences of using the Estelle language, and a simulation and validation tool, called Veda, to simulate and validate complex distributed algorithms for the distributed implementation of multi-rendezvous. Some design errors in published distributed rendezvous algorithms were found. We obtain from these experiences heuristic guidelines for trouble shooting of distributed algorithms.