Treffer: Petri Net Based Verification of Distributed Algorithms: An Example

A technique to describe and to verify distributed algorithms is suggested. This technique (based on Petri nets) reduces the modelling- and analysis effort to a reasonable expenditure. The paper outlines the technique along a typical network alogrithm, the echo algorithm. Keywords: Modelling, Correctness, Petri Nets, Verification Techniques, Temporal Logic. 1 Introduction A wide class of basic sequential algorithms (such as searching and sorting) can optimally be formulated in Pascal like programming notation and verified in the style of Hoare logic. A likewise generally accepted, integrated pair of techniques to formulate and verify distributed algorithms still remains to emerge. This paper is intended to contribute to this purpose. A distributed algorithm is adequately represented iff the employed operational primitives focus the essentials of its algorithmic idea. Hence the adequacy of a representation technique can best be demonstrated by help of a typical example. We have chose.