z-logo
Premium
Error‐preserving local transformations on communication protocols
Author(s) -
KapusKolar Monika
Publication year - 2013
Publication title -
software testing, verification and reliability
Language(s) - English
Resource type - Journals
SCImago Journal Rank - 0.216
H-Index - 49
eISSN - 1099-1689
pISSN - 0960-0833
DOI - 10.1002/stvr.449
Subject(s) - computer science , reachability , correctness , simple (philosophy) , protocol (science) , state (computer science) , queue , theoretical computer science , distributed computing , algorithm , computer network , medicine , philosophy , alternative medicine , epistemology , pathology
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.

This content is not available in your region!

Continue researching here.

Having issues? You can contact us here