Survey of protocol verification techniques based on finite state machine models

A survey is presented of techniques for verifying correctness properties of communications protocol design based on finite-state-machine (FSM) models. The conventional reachability analysis is first described, giving advantages and limitations. One major limitation is the so-called state-space explosion problem. To approach this and other problems, a survey of different approaches is presented. The author classifies the various techniques into categories. These include closed covers, localized protocol verification, divide-and-conquer, modified reachability analysis, and partial state exploration. Each technique is described in detail, including an analysis of its strengths and weaknesses. Based on this analysis, one technique is proposed as the basis for further work on a protocol verifier and analyzer workstation which is being designed as a protocol development tool.<>