Abstract:

We provide a verification of the distributed summing protocol using the cones and foci method. The protocol works in the context of a arbitrary connected network, where each node contains a number. The goal of the protocol is to let the root report the sum of the numbers of all elements. The protocol is interesting because it works in a highly nondeterministic way; althought the outcome is determined, it is unkown in what way it is obtained. It shows that the cones and foci method is capable of these kind of verifications. It should be noted that the proof that has been provided is based on process algebraic axioms and rules and as such can straightforwardly been computer checked (note added september 1998: the proof has been completely computer checked using PVS leading to one additional invariant and minor changes in another invariant).