Incorporating a partitioning algorithm into PROTEAN

Reachability analysis (RA) is the most popular protocol verification technique as it can verify a number of protocol properties, like deadlock freeness, livelock freeness and boundedness; and it can be easily automated. However, it is also very well-known that the state space explosion problem of RA limits its use in complex situations. The usefulness of existing verification tools in verifying complex protocols are very much pushed back by this problem. Various approaches have been proposed to tackle the problem; one of them is the partitioning method. So far, there has been very rare or possibly no report on how these methods can be implemented. This paper describes the implementation of the partitioning method into a proven computer-aided verification tool, PROTEAN, in order to address the state space explosion problem