Error‐preserving local transformations on communication protocols

SUMMARY Recently, two transformations were proposed for modifying a member of a closed system of communicating state machines (CSMs) without considering the other CSMs and nevertheless securing that after the modification, the system can reach the same dead states and overfill the same channels, where channels are assumed to be error‐free unidirectional first‐in‐first‐out queues. When verifying the general correctness properties of a communication protocol whose specification is such a system, one can employ the two error‐preserving local transformations (EPLTs) for simplifying individual CSMs and thereby the subsequent reachability analysis. The paper proves four new simple EPLTs and a generic EPLT which strongly generalizes all the six EPLTs and from which further easily applicable EPLTs can be derived simply by specialization. For each of the EPLTs, it also discusses how (non‐)executability of CSM transitions in the new system version reflects (non‐)executability of those in the old one. Copyright © 2011 John Wiley & Sons, Ltd.