Change search
ReferencesLink to record
Permanent link

Direct link
Verifying safety and deadlock properties of networks of asynchronously communicating processes
Number of Authors: 1
1988 (English)Report (Refereed)
Abstract [en]

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.

Place, publisher, year, edition, pages
Kista, Sweden: Swedish Institute of Computer Science , 1988, 1. , 18 p.
SICS Research Report, ISSN 0283-3638 ; R88:20
National Category
Computer and Information Science
URN: urn:nbn:se:ri:diva-14377OAI: diva2:1035665
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.Available from: 2016-10-13 Created: 2016-10-13

Open Access in DiVA

fulltext(2218 kB)0 downloads
File information
File name FULLTEXT01.pdfFile size 2218 kBChecksum SHA-512
Type fulltextMimetype application/pdf

Computer and Information Science

Search outside of DiVA

GoogleGoogle Scholar
The number of downloads is the sum of all downloads of full texts. It may include eg previous versions that are now no longer available

ReferencesLink to record
Permanent link

Direct link