Hierarchy-based incremental analysis of communication protocols
Kuo‐Chung Tai, Pramod V. Koppol · 2002
The authors present an incremental strategy for reachability analysis of communication protocols modeled as sets of communicating finite state machines (CFSMs) with synchronous communication and direct naming. A set of CFSMs is organized into a hierarchy. The authors present an algorithm that, for a given hierarchy of a set M of CFSMs, incrementally composes and reduces subsets of CFSMs in M and finally produces a minimum CFSM describing the external behavior of M. It is also showed that this incremental reachability analysis guarantees the detection of global deadlocks. An algorithm for selecting a hierarchy for a set of CFSMs and some empirical results are provided.>