The formalization and analysis of a communications protocol |
| |
Authors: | Glenn Bruns Stuart Anderson |
| |
Affiliation: | (1) Laboratory for Foundations of Computer Science, Computer Science Department, University of Edinburgh, EH9 3JZ Edinburgh, UK |
| |
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. |
| |
Keywords: | Safety Concurrency Formal methods Modal logic Model checking |
本文献已被 SpringerLink 等数据库收录! |