Abstract
In this paper, the notion of fair reachability is generalized to cyclic protocols with n > 2 communicating finite state machines. An equivalence is established between the set of fair reachable states and the set of reachable states with equal channel length. As a result, deadlock detection is decidable for cyclic protocols with finite fair reachability graphs. The concept of simultaneous unboundedness is defined and the lack of it is shown to be a necessary and sufficient condition for a cyclic protocol to have a finite fair reachability graph. For the first time, we are able to exactly characterize the class of protocols whose fair reachability graphs are finite. As far as decidability of deadlock detection is concerned, our result extends the class of cyclic protocols studied by Peng & Purushothaman, and complements the one investigated by Pachl. More importantly, our decision procedure is much more straightforward and efficient, as compared to Pachl’s and the one by Peng & Purushothaman. In this respect, we have improved the complexity of deadlock detection for the class of cyclic protocols with finite fair reachability graphs. To further demonstrate the strength of generalized fair reachability analysis, we also show that livelock detection is decidable for the class of cyclic protocols with finite fair reachability graphs.
Research reported in this paper was supported by NASA Center of Excellence in Space Data and Information Sciences Under USDA Subcontract No. 550-66.
Chapter PDF
Similar content being viewed by others
Keyword Codes
Keywords
References
D. Brand and P. Zafiropulo, “On Communicating Finite-State Machines,” Journal of ACM, Vol. 30, No. 2, April 1983, pp. 323–342.
L. Cacciari and O. Rafiq, “On Improving Reduced Reachability Analysis,” Proc. Fifth International Conference on Formal Description Techniques for Distributed Systems and Communications Proto-
cols–FORTE’92, Perros-Guirec, France, October 13–16, 1992, M. Daiz and R. Groz (Ed.), Elsevier Science Publishers B.V. ( North-Holland ), 1992, pp. 137–152.
L. Cacciari and O. Rafiq, “Decidability Issues in Reduced Reachability Analysis,” Proc. 1993 International Conference on Network Protocols, San Francisco, CA, October 19–22, 1993, pp. 158–165.
T.Y. Choi and R.E. Miller, “Protocol Analysis and Synthesis by Structured Partitions,” Computer Networks and ISDN Systems, Vol. 11, 1986, pp. 367–381.
H. Liu and R.E. Miller, “Deadlock Detection for Cyclic Protocols Using Generalized Fair Reachability Analysis,” Technical Report CS-TR-3135, Dept. of Computer Science, Univ. of Maryland at College Park, September 1993.
H. Liu and R.E. Miller, “Generalized Fair Reachability Analysis for Cyclic Protocols: Part 1,” Technical Report CS-TR-3204, Dept. of Computer Science, Univ. of Maryland at College Park, January 1994.
H. Liu and R.E. Miller, “Generalized Fair Reachability Analysis for Cyclic Protocols: Decidability for Logical Correctness Problems,” March 1994, submitted for publication.
M.G. Gouda, C.H. Chow, and S.S. Lam, “Livelock Detection in Networks of Communicating Finite State Machines,” Technical Report, TR-84–10, Dept. of Computer Science, Univ. of Texas at Austin, April 1984.
M.G. Gouda, C.H. Chow, and S.S. Lam, “On the Decidability of Livelock Detection in Networks of Communicating Finite State Machines,” Proc. Protocol Specification, Testing and Verification, IV, Y. Yemini, R. Strom, and S. Yemini (Ed.), Elsevier Science Publishers B.V. ( North-Holland ), 1985, pp. 47–56.
M.G. Gouda and J.Y. Han, “Protocol Validation by Fair Progress State Exploration,” Computer Networks and ISDN Systems, Vol. 9, 1985, pp. 353–361.
M.G. Gouda and Y.T. Yu, “Protocol Validation by Maximal Progress State Exploration,” IEEE Transactions on Communications, Vol. COM-32, No. 1, 1984, pp. 94–97.
K. Okumura, “Protocol Analysis from Language Structure,” Proc. Protocol Specification, Testing and Verification, VIII, S. Aggarwal and K. Sabnani (Ed.), Elsevier Science Publishers B.V. ( North-Holland ), 1988, pp. 113–124.
J. Pachl, “Reachability Problems for Communicating Finite State Machines,” Research Report, CS-82–12, Dept. of Computer Science, Univ. of Waterloo, May, 1982
J. Pachl, “Protocol Description and Analysis Based on a State Transition Model with Channel Expressions,” Proc. Protocol Specification, Testing and Verification, VII, J. Rubin and C.H. West (Ed.), Elsevier Science Publishers B.V. ( North-Holland ), 1987, pp. 207–219.
[15] W. Peng, “Single-Link Communicating Finite State Machines,” Dept. of Computer Science, Southwest Texas State Univ., October, 1993, private communication.
W. Peng and S. Purushothaman, “A Unified Approach to the Deadlock Detection Problem in Networks of Communicating Finite State Machines,” Proc. of 2nd International Conference, CAV’90, New Brunswick, N.J., June, 1990, E.M. Clarke and R.P.Kurshan (Ed.), Lecture Notes in Computer Science, Vol. 531, pp. 243–252.
W. Peng and S. Purushothaman, “Data Flow Analysis of Communicating Finite State Machines,” ACM Transactions on Programming Languages and Systems, Vol. 13, No. 3, 1991, pp. 399–442.
J. Rubin and C.H. West, “An Improved Protocol Validation Technique,” Computer Networks and ISDN Systems, Vol. 6, 1982, pp. 65–73.
D. Sidhu, A. Chung, and T.P. Blumer, “Experience with Formal Methods in Protocol Development,” ACM SIGCOMM, Computer Communication Review, Vol$121, No. 2, April, 1991, pp. 81–101.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1995 Springer Science+Business Media Dordrecht
About this chapter
Cite this chapter
Liu, H., Miller, R.E. (1995). Generalized Fair Reachability Analysis for Cyclic Protocols: Part 1. In: Vuong, S.T., Chanson, S.T. (eds) Protocol Specification, Testing and Verification XIV. IFIP Advances in Information and Communication Technology. Springer, Boston, MA. https://doi.org/10.1007/978-0-387-34867-4_18
Download citation
DOI: https://doi.org/10.1007/978-0-387-34867-4_18
Publisher Name: Springer, Boston, MA
Print ISBN: 978-1-4757-6308-9
Online ISBN: 978-0-387-34867-4
eBook Packages: Springer Book Archive