Implementation of a verification method to communication protocols
Number of Authors: 1
1989 (English)Report (Refereed)
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
Computer and Information Science
IdentifiersURN: urn:nbn:se:ri:diva-21421OAI: oai:DiVA.org:ri-21421DiVA: diva2:1041457
Original report number T89010.2016-10-312016-10-31Bibliographically approved