This paper presents a parallel protocol verification algorithm for checking the logical correctness of computer network protocols modeled as a collection of communicating finite state machines (CFSM) with first in first out (FIFO) queues. The method of parallelizing the automated reachability analysis in MIMD distributed memory message passing environment is a new approach to reduce the complexity of analyzing non-trivial protocols. A parallel algorithm has been developed to generate and search the different sub-trees of the reachability tree simultaneously in different processors. The software tool employs parallel reachability analysis of computer network protocols, modeled as a network of CFSMs and FIFO queues, for checking their logical correctness. It is written in Occam, and implements this procedure on a transputer based system and the results obtained from the verification of various protocols using a few available transputers are extrapolated to predict the performance gain achievable for a still larger configuration of similar nodes. This multi-processing approach can be combined with suitable search strategies to contain state explosion in reachability analysis, in order to further improve the overall system performance. Moreover the technique is general enough to be ported on various distributed processing system using general high level language such as PVM and C respectively.
展开▼
