Communication protocols pose interesting and difficult challenges for verification technologies. The state spaces of interesting protocols are either infinite or too large for finite-state verification techniques like model checking and state exploration. Theorem proving is also not effective since the formal correctness proofs of these protocols can be long and complicated. We describe a series of protocol verification experiments culminating in a methodology where theorem proving is used to abstract out the sources of unboundedness in the protocol to yield a skeletal protocol that can be verified using model checking.
Our experiments focus on the Philips bounded retransmission protocol originally studied by Helmink, Sellink, and Vandraager. First, a scaled-down version of the protocol is analyzed using the MurΦ, state exploration tool as a debugging aid and then translated into the PVS specification language. The PVS verification of the generalized protocol illustrates the difficulty of using theorem proving to verify infinite-state protocols. A large part of this difficulty can be overcome by extracting a finite-state abstraction of the protocol that preserves the property of interest while being amenable to model checking. We compare the performance of MurΦ, SMV, and the PVS model checkers on this reduced protocol.
R&D Divisions