Error‐preserving local transformations on communication protocols. (21st January 2011)

• Record Type: Journal Article
• Authors: Kapus‐Kolar, Monika
• Is Part Of: Software testing, verification & reliability. Volume 23:Number 1(2013:Jan.)
• Page Start: 3
• Page End: 25
• Publication Date: 2011-01-21
• Subjects: Computer software -- Testing -- Periodicals; Computer software -- Verification -- Periodicals; Computer software -- Reliability -- Periodicals; 005.14
• DOI: 10.1002/stvr.449
• Languages: English
• ISSNs: 0960-0833

Abstract

<abstract abstract-type="main" xml:lang="en" id="stvr449-abs-0001"> <title>SUMMARY</title> <p id="stvr449-para-0001">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 &amp; Sons, Ltd.</p> </abstract>