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-22189OAI: diva2:1041733
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-31 Created: 2016-10-31

Open Access in DiVA

fulltext(2218 kB)7 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
Total: 7 downloads
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

Total: 1 hits
ReferencesLink to record
Permanent link

Direct link