Accession Number : ADA192726

Title :   A Modular Proof of Correctness for a Network Synchronizer.

Descriptive Note : Technical rept.,

Corporate Author : MASSACHUSETTS INST OF TECH CAMBRIDGE LAB FOR COMPUTER SCIENCE

Personal Author(s) : Fekete, A ; Lynch, N ; Shira, L

PDF Url : ADA192726

Report Date : Sep 1987

Pagination or Media Count : 75

Abstract : In this paper we offer a formal, rigorous proof of the correctness of Awerbuch's algorithm for network synchronization. We specify both the algorithm and the correctness condition using the I/O automation model, which has previously been used to describe and verify algorithms for concurrency control and resource allocation. We show that the model is also a powerful tool for reasoning about distributed graph algorithms. Our proof of correctness follows closely the intuitive arguments made by the design techniques as stepwise refinement and modularity. In particular, since the algorithm uses simpler algorithms for synchronization within and between 'clusters' of nodes, our proof can import as lemmas the correctness of these simpler algorithms. Keywords: Verification, Modularity, Network protocols, and Synchronization.

Descriptors :   *NETWORKS, *SYNCHRONIZATION(ELECTRONICS), *INPUT OUTPUT MODELS, *COMPUTER COMMUNICATIONS, ALGORITHMS, ALLOCATIONS, AUTOMATION, CLUSTERING, DISTRIBUTION, GRAPHS, MODULAR CONSTRUCTION, NODES, REASONING, RESOURCE MANAGEMENT, SYNCHRONISM

Subject Categories : Computer Hardware

Distribution Statement : APPROVED FOR PUBLIC RELEASE