The formalization and analysis of a communications protocol

Glenn Bruns, Stuart Anderson

Research output: Contribution to journalArticlepeer-review


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
Issue number1
Publication statusPublished - 1994


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


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

Cite this