Skip to content
University of Maryland LibrariesDigital Repository at the University of Maryland
    • Login
    View Item 
    •   DRUM
    • College of Computer, Mathematical & Natural Sciences
    • Computer Science
    • Technical Reports of the Computer Science Department
    • View Item
    •   DRUM
    • College of Computer, Mathematical & Natural Sciences
    • Computer Science
    • Technical Reports of the Computer Science Department
    • View Item
    JavaScript is disabled for your browser. Some features of this site may not work without it.

    Generalized Fair Reachability Analysis for Cyclic Protocols

    Thumbnail
    View/Open
    CS-TR-3421.ps (321.5Kb)
    No. of downloads: 290

    Auto-generated copy of CS-TR-3421.ps (284.7Kb)
    No. of downloads: 551

    Date
    1998-10-15
    Author
    Liu, Hong
    Miller, Raymond E.
    Metadata
    Show full item record
    Abstract
    In this paper, the notion of fair reachability is generalized to cyclic protocols with $n\geq 2$ machines. Substantial state reduction can be achieved via fair progress state exploration. It is shown that the fair reachable state space is exactly the set of reachable states with equal channel length. As a result, deadlock detection is decidable for ${\cal P}$, the class of cyclic protocols whose fair reachable state spaces are finite. The concept of simultaneous unboundedness is defined and the lack of it is shown to be a necessary and sufficient condition for a protocol to be in ${\cal P}$. Through finite extension of the fair reachable state space, it is also shown that detection of unspecified receptions, unboundedness, and nonexecutable transitions are all decidable for ${\cal P}$. Furthermore, it is shown that any protocol ${\cal P}$ is logically correct if and only if there is no logical error in its fair reachable state space. This study shows that for the class ${\cal P}$, our generalized fair reachability analysis technique not only achieves substantial state reduction but also maintains very competitive logical error coverage. Therefore, it is a very useful technique to prove logical correctness for a wide variety of cyclic protocols.
    URI
    http://hdl.handle.net/1903/423
    Collections
    • Technical Reports of the Computer Science Department

    DRUM is brought to you by the University of Maryland Libraries
    University of Maryland, College Park, MD 20742-7011 (301)314-1328.
    Please send us your comments.
    Web Accessibility
     

     

    Browse

    All of DRUMCommunities & CollectionsBy Issue DateAuthorsTitlesSubjectsThis CollectionBy Issue DateAuthorsTitlesSubjects

    My Account

    LoginRegister
    Pages
    About DRUMAbout Download Statistics

    DRUM is brought to you by the University of Maryland Libraries
    University of Maryland, College Park, MD 20742-7011 (301)314-1328.
    Please send us your comments.
    Web Accessibility