SODA

Verifying safety and deadlock properties of networks of asynchronously communicating processes

Orava, Fredrik (1988) Verifying safety and deadlock properties of networks of asynchronously communicating processes. [SICS Report]

[img]
Preview
PDF
2218Kb

Abstract

We present a method for specifying and verifying networks of non-deterministic processes that communicate by asynchronous message-passing. The method handles safety and deadlock properties. Networks are specified in an operational manner by transition systems. We say that the specification A implements another specification B if every safety and deadlock property true of A also is true of B. We establish a proof rule for verifying that A implements B in this sense. The proof rule is based on simulation between the states of A and B, and is shown to be complete under the assumption that B is deterministic. We illustrate the method by applying it to the alternating bit protocol.

Item Type:SICS Report
Additional Information:Also located in the Proceedings of the 9th International Symposium on Protocol Specification, Testing and Verification, June 1989, Enschede, Holland. Brinksma, Scollo and Vissers, editors, published by North-Holland Press. Original report number R88020.
ID Code:2527
Deposited By:Vicki Carleson
Deposited On:22 Sep 2009
Last Modified:18 Nov 2009 16:10

Repository Staff Only: item control page