Abstract
In this paper, we propose a parallel step exploration technique for protocol validation in the context of protocol composition. A protocol is modeled as a network of extended communicating finite state machines (ECFSM’s). A composite protocol is defined as an interleaved execution of a set of component protocols subject to a set of constraints such as synchronization, ordering and inhibition. By encoding the constraints into the component protocols and the analysis algorithm, our method keeps each process in the component protocols as a separate entity and performs validation without constructing the composite protocol explicitly. We show that our technique not only achieves significant state reduction but also preserves the progress property of the composite protocol in the reduced state space. To our best knowledge, this is the first attempt to adapt existing state reduction techniques to the validation of protocol composition.
This work was supported by NSF under grants CCR9211621 end CCR9502506.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
L. Cacciari and O. Rafiq, “On Improving Reduced Reachability Analysis,” Proc. FORTE’92, Perros-Guirec, France, October 13–16, 1992, pp. 137–152.
C.H. Chow, M.G. Gouda and S.S. Lam, “A Discipline for Constructing Multi-Phase Communicating Protocols,” ACM Trans. Comput. Syst., 3 (4), 1985, pp. 315–343.
T.Y. Choi and R.E. Miller, “Protocol Analysis and Synthesis by Structured Partitions”, Computer Networks and ISDN Systems, 11, 1986, pp. 367–381.
M. Gouda and J.Y. Han, “Protocol Validation by Fair Progress State Exploration,” Computer Networks and ISDN Systems, 9, 1985, pp. 353–361.
P. Godefroid and P. Wolper, “Using Partial Orders for the Efficient Verification of Deadlock Freedom and Safety Properties,” Formal Methods in System Design, 2 (2), 1993.
P. Godefroid and P. Wolper, “A Partial Approach to Model Checking,” Information and Computation, 110 (2), 1994, pp. 305–326.
HGW92] G. Holzmann, P. Godefroid and P. Wolper, “Coverage Preserving Reduction Strategies for Reachability Analysis,” PSTV’92.
M. Itoh and H. Ichikawa, “Protocol Verification Algorithm Using Reduced Reachability Analysis,” Trans. IECE of Japan, E66 (2), 1983, pp. 88–93.
H.A. Lin, “A Methodology for Constructing Communication Protocols with Multiple Concurrent Functions,” Distributed Computing, 3 (1), 1988, pp. 23–40.
H.A. Lin, “Constructing Protocols with Alternative Functions,” IEEE Transactions on Computers, 40 (4), 1991, pp. 376–386.
H.A. Lin and C.L. Tarng, “An Improved Method for Constructing Multiphase Communications Protocols,” IEEE Transactions on Computers, 42 (1), 1993, pp. 15–26.
H. Liu and R. Miller, “Generalized Fair Reachability for Cyclic Protocols,” IEEE/ACM Transactions on Networking, 4 (2), April 1996, pp. 192–204.
H. Liu and R.E. Miller, “An Approach to Cyclic Protocol Validation,” Computer Communications, 19 (14), 1996, pp. 1175–1187.
H. Liu and R.E. Miller, “Partial-Order Validation for Multi-Process Protocols Modeled as Communicating Finite State Machines,” Proc. ICNP’96, Oct. 29 Nov. 1, 1996, pp. 76–83.
K. Ozdemir and H. Ural, “Deadlock Detection in CFSM Models via Simultaneously Executable Sets,” ICCI’94, Peterborough, Ontario, Canada, May 1994, pp. 673–688.
P93] D. Peled, “All from One, One for All: On Model Checking Using Representatives,” CAV’93.
P94] D. Peled, “Combining Partial Order Reduction with On-the-fly Model-Checking,” CAV’94.
J. Rubin and C.H. West, “An Improved Protocol Validation Technique,” Computer Networks, 6, 1982, pp. 65–73.
G. Singh, “A Compositional Approach for Designing Protocols,” Proc. ICNP’93, San Francisco, CA, October 19–22, 1993, pp. 98–105.
G. Singh and M. Sammeta, “On the Construction of Multiphase Protocols,” Proc. ICNP’94, Boston, MA, October 25–28, 1994, pp. 151–158.
S94b] G. Singh, “A Methodology for Constructing Communication Protocols,” Proc. ACM SIGCOMM’94, August 31 — September 2, 1994, London, U.K., pp. 245–255.
SL97] G. Singh and H. Liu, “Validating Protocol Composition for Progress by Parallel Step Reach-ability Analysis,” in preparation.
H.v.d. Schoot and H. Ural, “Protocol Verification by Leaping Reachability Analysis,” Proc. IC3N’96, Rockville, MD, USA, October 16–19, 1996, pp. 334–339.
V90] A. Valmari, “A Stubborn Attack on State Explosion,” Proc. CAV’90.
Y.T. Yu and M.G. Gouda, “Deadlock Detection for a Class of Communicating Finite State Machines,” IEEE Transactions on Communications, 30 (12), 1982.
ZB86] J.R. Zhao and G.v. Bochmann, “Reduced Reachability Analysis of Communication Protocols: a New Approach,” Proc. PSTV’86, pp. 243–254.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1997 Springer Science+Business Media Dordrecht
About this chapter
Cite this chapter
Singh, G., Liu, H. (1997). Validating Protocol Composition for Progress by Parallel Step Reachability Analysis. In: Mizuno, T., Shiratori, N., Higashino, T., Togashi, A. (eds) Formal Description Techniques and Protocol Specification, Testing and Verification. IFIP — The International Federation for Information Processing. Springer, Boston, MA. https://doi.org/10.1007/978-0-387-35271-8_15
Download citation
DOI: https://doi.org/10.1007/978-0-387-35271-8_15
Publisher Name: Springer, Boston, MA
Print ISBN: 978-1-4757-5260-1
Online ISBN: 978-0-387-35271-8
eBook Packages: Springer Book Archive