Formal Specification and Verification of Distributed Systems.

Abstract

The authors develop an event-based model to specify formally the behavior (the external view) and the structure (the internal view) of distributed systems. Both control-related and data-related properties of distributed systems are specified using two fundamental relationships among events; the 'happens before' relation, representing time order; and the 'enabling' relation, representing causality. No assumption about the existence of a global clock is made in the specifications. The correctness of a design can be proved before implementation by checking the consistency between the behavior specification and the structure specification of a system. Important properties of concurrent systems such as 'mutual exclusion', 'concurrency', and other 'safety' and 'liveness' properties can be specified and verified.

Open PDF

Document Details

Document Type
Technical Report
Publication Date
Jun 01, 1982
Accession Number
ADA120204

Entities

People

  • Bo-shoe Chen
  • Raymond T. Yeh

Organizations

  • University of Maryland

Tags

Communities of Interest

  • Energy and Power Technologies

DTIC Thesaurus Topics

  • Air Force
  • Computations
  • Computer Networks
  • Computer Programs
  • Computer Science
  • Computers
  • Consistency
  • Environment
  • Explosions
  • Information Science
  • Language
  • Maryland
  • Multithreading
  • Network Protocols
  • Sequences
  • Software Development
  • Universities

Fields of Study

  • Computer science
  • Engineering

Readers

  • Artificial Intelligence
  • Mathematical Modeling and Probability Theory.