Proving Safety and Liveness of Communicating Processes with Examples.

Abstract

A method is proposed for reasoning about safety and liveness properties of message passing networks. The method is hierarchical and is based upon combining the specifications of component processes to obtain the specification of a network. The inference rules for safety properties use induction on the number of messages transmitted; liveness proofs use techniques similar to termination proofs in sequential programs. The authors illustrate the method with two examples: concatenations of buffers to construct larger buffers and a special case of Stenning protocol for message communication over noisy channels.

Open PDF

Document Details

Document Type
Technical Report
Publication Date
Aug 01, 1982
Accession Number
ADA120372

Entities

People

  • J. Misra
  • K. M. Chandy
  • Todd Smith

Organizations

  • University of Texas at Austin

Tags

Communities of Interest

  • Energy and Power Technologies
  • Materials and Manufacturing Processes

DTIC Thesaurus Topics

  • Air Force
  • Classification
  • Communication Networks
  • Computer Communications
  • Computer Science
  • Computers
  • Consumers
  • Distributed Computing
  • Environment
  • Hierarchies
  • Networks
  • Reasoning
  • Scientific Research
  • Sequences
  • Specifications
  • Transmitters
  • Universities

Fields of Study

  • Computer science

Readers

  • Computer Networking
  • Mathematical Modeling and Probability Theory.

Technology Areas

  • AI & ML
  • AI & ML - Machine Learning Algorithms