Change search
ReferencesLink to record
Permanent link

Direct link
Implementation of a verification method to communication protocols
Number of Authors: 1
1989 (English)Report (Refereed)
Abstract [en]

It is important to reason about a number of desirable protocol properties to ensure correctness of a designed communicating system. Such properties can be formulated in some temporal logic. If the specification of a communicating system is finite-state, that is, the system has a finite number of distinct states, it is often possible to verify automatically by an efficient algorithm, called a model checking algorithm, whether the system satisfies a property expressed in the logic. We describe a model checking method for Communicating Systems. An implementation of this model-checking facility is obtained by combining two automated tools, namely, CWB (the Concurrency Workbench developed at Edinburgh, Sussex and SICS) and EMC (the Extended Model Checker developed by Emerson and Clarke). In the EMC, there is an efficient model checking algorithm for branching time temporal logic(CTL) with the standard semantics. We change the standard semantics for CTL in terms of communication actions. We implement a transformation of the transition graph into a finite number of distinct states so that it can be fed into EMC to use our logic.

Place, publisher, year, edition, pages
Swedish Institute of Computer Science , 1989, 1. , 41 p.
SICS Technical Report, ISSN 1100-3154 ; T89:10
National Category
Computer and Information Science
URN: urn:nbn:se:ri:diva-21421OAI: diva2:1041457
Original report number T89010.Available from: 2016-10-31 Created: 2016-10-31

Open Access in DiVA

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

Computer and Information Science

Search outside of DiVA

GoogleGoogle Scholar
Total: 5 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: 5 hits
ReferencesLink to record
Permanent link

Direct link