The formalization and analysis of a communications protocol

Glenn Bruns, Stuart Anderson

Research output: Contribution to journalArticlepeer-review

Abstract

The MSMIE protocol [SBC89] allows processors in a distributed system to communicate via shared memory. It was designed to meet the reliability and efficiency needs of applications such as nuclear safety systems. We present a formal model of the MSMIE protocol expressed in the notation CCS. Desirable properties of the protocol are expressed in the modal mu-calculus, an expressive modal logic. We show that the protocol lacks an important liveness property. In actual operation, additional operating constraints are checked to avoid potential problems. We present a modified protocol and show that it possesses the liveness property even without checking operating constraints. We also show how parts of the analysis were automated with the Concurrency Workbench.
Original languageEnglish
Pages (from-to)92-112
Number of pages21
JournalFormal Aspects of Computing
Volume6
Issue number1
DOIs
Publication statusPublished - 1994

Keywords

  • Safety
  • Concurrency
  • Formal methods
  • Modal logic
  • Model checking

Fingerprint

Dive into the research topics of 'The formalization and analysis of a communications protocol'. Together they form a unique fingerprint.

Cite this