APPLYING A NEW DECOMPOSITION METHOD TO VERIFY COMMUNICATION PROTOCOLS

Reachability analysis has proved to be one of most effective methods f or protocol verification, but it is well known that it suffers from th e state space explosion problem. Various approaches have been proposed to tackle the problem; and, so far, there have been very few reports on the applications of these techniques. We have proposed a new approa ch to generating state space in order to help relieve the state space explosion problem. In this approach, state space is generated and veri fied in stages. That is, only one subspace is involved in each stage o f verification; upon completion, the memory occupied by a particular s ubspace can be released and subsequently used by the next subspace. Th e amount of memory needed for the verification of the whole protocol c an be dramatically reduced, and thus the explosion problem relieved. T his paper discusses the application of this technique to verify the Al ternating Bit Protocol and the real-life ISO ACSE protocol, and aims t o present a successful case where protocol verification and its associ ated technique can be applied to a contemporary industrial problem-hid den errors in protocol specifications. (C) 1998 Elsevier Science Inc.