A termination detection algorithm: Specification and verification

Abstract

We propose a methodology for the specification and verification of distributed algorithms using Gurevich’s concept of Abstract State Machines. The methodology relies on a distinction between a higher- level specification and a lower-level specification of an algorithm. The algorithm is characterized by an informal problem description. A justification assures the appropriateness of the higher-level specification for the problem description. A mathematical verification assures that the lower-level specification implements the higher-level one and is based on a refinement-relation. This methodology is demonstrated by a well- known distributed termination detection algorithm originally invented by Dijkstra, Feijen, and van Gasteren.