Premium
Error‐preserving reductions on communication protocols
Author(s) -
Duan Lihua,
Chen Jessica
Publication year - 2008
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.385
Subject(s) - reachability , computer science , model checking , variety (cybernetics) , state (computer science) , process (computing) , transformation (genetics) , formal methods , communications protocol , distributed computing , theoretical computer science , programming language , artificial intelligence , computer network , biochemistry , chemistry , gene
Abstract Common logical design errors in communication protocols are typically detected through reachability analysis or state‐based model checking techniques. These techniques suffer from a state explosion problem and a variety of methods have been explored to deal with it. In this paper, two transformation rules are proposed to be applied specifically on the specifications of communication protocols to reduce their sizes while preserving common logical design errors. These rules are applied on the specification of each individual process in the protocols before state exploration and thus can be combined with most of the existing reachability analysis or model checking techniques applied during state exploration . Copyright © 2007 John Wiley & Sons, Ltd.