Skip Navigation


The Computer Journal Advance Access originally published online on May 12, 2006
The Computer Journal 2006 49(5):541-553; doi:10.1093/comjnl/bxl017
This Article
Right arrow Full Text
Right arrow Full Text (PDF)
Right arrow Colour version of Figure 7
Right arrow All Versions of this Article:
49/5/541    most recent
bxl017v1
Right arrow Alert me when this article is cited
Right arrow Alert me if a correction is posted
Services
Right arrow Email this article to a friend
Right arrow Similar articles in this journal
Right arrow Similar articles in ISI Web of Science
Right arrow Alert me to new issues of the journal
Right arrow Add to My Personal Archive
Right arrow Download to citation manager
Right arrow Search for citing articles in:
ISI Web of Science (1)
Right arrowRequest Permissions
Google Scholar
Right arrow Articles by Ye, Q.
Right arrow Articles by Kung, D.
Right arrow Search for Related Content
Social Bookmarking
Add to CiteULike   Add to Connotea   Add to Del.icio.us  
What's this?

© The Author 2006. Published by Oxford University Press on behalf of The British Computer Society. All rights reserved. For Permissions, please email: journals.permissions@oxfordjournals.org

A Blocking-based Approach to Protocol Validation

Qizhi Ye, Yu Lei* and David Kung

Department of Computer Science and Engineering, University of Texas at Arlington Arlington, TX 76019-0015, USA

*Corresponding author: ylei{at}cse.uta.edu

Reachability analysis is a commonly used approach to protocol validation, but it suffers from the well-known state explosion problem. In this paper, we present a new approach to reachability analysis called blocking-based simultaneous reachability analysis (or BSRA). A central notion in BSRA is that of a global blocking point. Instead of exploring every global state, BSRA only explores a set of global blocking points, which usually account for a small portion of the state space. We show how to use BSRA to detect several commonly found logical errors. Our experimental results demonstrate that BSRA can significantly reduce the number of states explored during protocol validation.

Key Words: Protocol validation • reachability analysis • deadlocks • channel overflows • unspecified receptions • non-executable transitions


Add to CiteULike CiteULike   Add to Connotea Connotea   Add to Del.icio.us Del.icio.us    What's this?




Disclaimer:
Please note that abstracts for content published before 1996 were created through digital scanning and may therefore not exactly replicate the text of the original print issues. All efforts have been made to ensure accuracy, but the Publisher will not be held responsible for any remaining inaccuracies. If you require any further clarification, please contact our Customer Services Department.