## 摘要

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.

原文 | English |
---|---|

頁（從 - 到） | 184-192 |

頁數 | 9 |

期刊 | Proceedings - IEEE Computer Society's International Computer Software & Applications Conference |

DOIs | |

出版狀態 | Published - 1 12月 1989 |

事件 | Proceedings of the Thirteenth Annual International Computer Software & Applications Conference - COMPSAC 89 - Orlando, FL, USA 持續時間: 20 9月 1989 → 22 9月 1989 |