A Spanning Tree Object-Oriented Distributed Algorithm: Specification and Proof

This paper presents a way to specify, to prove, and to implement object-oriented distributed cooperative algorithms. Our method gathers together three kinds of tools or formal concepts. It is derived from the B Method. So it uses a refinement approach and a proof of each specification step. The second set of concepts comes from distributed artificial intelligence. One main aspect of parallel and distributed computation is the uncertainty of the knowledge state of other sites. To express it, an epistemic logic is used to define knowledge of sites. Finally we consider some interesting practical results of distributed algorithms research. The method defines an application from three points of view (group, object, and method levels). A particular state automata formalism is used for each specification step. Finally, a distributed spanning tree algorithm i s developed.