|Final Report of the COST-247 Action|
A verification of a distributed summing protocol
Jan Friso Groote
|Centrum voor Wiskunde en Informatica|
|Specification and Analysis of Embedded Systems|
|P.O. Box 94079|
|1090 GB Amsterdam|
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).
This presentation has been given during the COST-247 9th Management Committee Meeting (Antalya, Turkey, November 4--5, 1996).
COST-247 Working Group(s):
This Page was prepared by Mark Jorgensen.