Fourth International Conference on Network Protocols (ICNP'96)
Partial-Order Validation for Multi-Process Protocols Modeled as Communicating Finite State Machines
Columbus, Ohio
October 29-November 01
ISBN: 0-8186-7453-9
In this paper, we adapt the partial order state reduction techniques developed for Petri nets and labeled transition systems to the validation ofmulti-process protocols modeled as communicating finite state machines. We identify two specific partial order reduction methods in this context: (1) maximal partial order reachability analysis, which is a generalization of maximal reachability analysis to protocols with n\ge 2 processes; and (2) simultaneous partial order reachability analysis, which is a counterpart of fair reachability analysis for protocols with n\ge 2 processes and arbitrary communication topologies. We study the logical error detection capabilities of each method and show that these two methods, when used together, provide complete logical error coverage for bounded multi-process protocols.
Index Terms:
Network Protocols; Communicating Finite State Machines; Protocol Validation; Reachability Analysis; State Explosion; Fair Reachability Analysis; Maximal Reachability Analysis; Partial Order State Reduction Techniques
Citation:
Hong Liu, Raymond E. Miller, "Partial-Order Validation for Multi-Process Protocols Modeled as Communicating Finite State Machines," icnp, pp.76, Fourth International Conference on Network Protocols (ICNP'96), 1996