A Modular Proof of Correctness for a Network Synchronizer.

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.

Open PDF

Document Details

Document Type
Technical Report
Publication Date
Sep 01, 1987
Accession Number
ADA192726

Entities

People

  • A. Fekete
  • L. Shira
  • N. Lynch

Organizations

  • Massachusetts Institute of Technology

Tags

Communities of Interest

  • Advanced Electronics
  • Weapons Technologies

DTIC Thesaurus Topics

  • Algorithms
  • Automata
  • Classification
  • Communication Systems
  • Computer Networks
  • Computer Science
  • Computers
  • Contracts
  • Environment
  • Information Processing
  • Massachusetts
  • Military Research
  • Network Protocols
  • Networks
  • Security
  • Sequences
  • Specifications

Fields of Study

  • Computer science

Readers

  • Adaptive Control and Estimation with Uncertainty in Dynamic Systems.
  • Computer Networking
  • Software Engineering.