Parallel protocol verification using the two-phase algorithm

Maria C. Yuang*, A. Kershenbaum


研究成果: Conference article同行評審

2 引文 斯高帕斯(Scopus)


A parallel protocol verification algorithm, called the two-phase algorithm, is proposed in an attempt to provide a maximum of verification with a minimum of state space. Rather than compose all communicating finite-state machines (FSMs) into one large global reachability tree, the two-phase algorithm constructs a local expanded tree for each FSM augmented with external information. The first phase of the algorithm performs the expanded tree construction, and the second phase performs error detection based on the constructed expanded trees. By separating verification into two phases, the algorithm allows verification for all FSMs to be executed in parallel. The algorithm thus requires smaller run-time. Moreover, by introducing a new method for the construction of the expanded trees, the algorithm requires fewer explored states. The algorithm can verify protocols with any number of processes. Verification for protocols with more than two processes is illustrated.


深入研究「Parallel protocol verification using the two-phase algorithm」主題。共同形成了獨特的指紋。