Khan, Ahmed Hussain (1989) Implementation of a verification method to communication protocols. [SICS Report]
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.
|Item Type:||SICS Report|
|Additional Information:||Original report number T89010.|
|Deposited By:||Vicki Carleson|
|Deposited On:||29 Oct 2007|
|Last Modified:||18 Nov 2009 16:00|
Repository Staff Only: item control page