Abstract
An important method for testing large and complex protocols repeatedly generates and tests a part of the reachable state space by following a random walk; the main advantage of this method is that it has minimal memory requirements. We use the coupling technique from Markov chain theory to show that short trajectories of the random walk sample accurately the reachable state space of a nontrivial family of protocols, namely, the symmetric dyadic flip-flops. This is the first evidence that the random walk method is amenable to rigorous treatment.
Following West's original reasoning, efficient sampling of the reachable state space by random walk suffices to ensure effectiveness of testing. Is, however, efficient sampling of the random walk necessary for the effectiveness of the random walk method? In the context of Markov chain theory, “small cover time” can be thought of as a simpler justification for the effectiveness of testing by random walk; all symmetric (reversible) protocols possess the small cover time property.
Thus the conclusions of our work are that (i) the random walk method can be understood in the context of known Markov chain theory, and (ii) symmetry (reversibility) is a general protocol style that supports testing by random simulation.
Research supported by the National Science Foundation.
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
Aldous, D., “Random Walks on finite groups and rapidly mixing Markov chains”, Seminaire de Probabilites XVII, Lecture Notes in Mathematics, Vol. 986, Springer Ferlag, Berlin, 1983.
Aldous, D., “On the Markov Chain Simulation Method for uniform combinatorial distributions and simulated annealing”, Probability in Eng. and Inf. Sci. 1, 1987, pp 33–46.
Aleliunas, R., Karp, R.M., Lipton, J.R., Lovasz, L., and Rackoff, C., “Random walks, universal traversal sequences, and the complexity of maze problems”, Proc. 20th IEEE Symp. on Foundations of Computer Science, 1979, 218–233.
Apt, K.R., and Kozen, D.Z., “Limits for automatic verification of finite state concurrent systems”, Inf. Processing Letters, Vol. 22. No. 6, 1986, pp. 307–309.
Broder, A.Z., “How hard is it to marry at random? Approximating the Permanent”, Proc. 18th ACM Symp. on the Theory of Computing, 1986, pp. 55–58.
Broder, A.Z., “Generating random Spanning Trees”, Proc. 30th IEEE Symp. on Foundations of Computer Science, 1989, pp 4422–447.
Cohen, E., Mihail, M., Papadimitriou, C.H., and Tsantilas, T., “Testing Protocols by Random Walk: Mixing and Cover Times”, Bellcore TM ARA-4-94, 1994.
Browne, M.C., Clarke, E.M., Dill, D.L., and Mishra, B., “Automatic verification of sequential circuits using temporal logic”, IEEE Trans. on Computers, Vol. C-35, No. 12, 1986, pp. 1035–1043.
Clarke, E.M., Emerson, E.A., and Sisla, A.P., “Automatic verification of finite state concurrent systems using temporal logic specifications: a practical approach”, Proc. 10th ACM Symposium on Principles of Programming Languages, 1983.
Diaconis, P., “Group Theory and Statistics”, Lecture Notes from a course taught at Harvard, Spring 1982.
Dyer, M., Frieze, A., and Kannan, R., “A random polynomial time algorithm for estimating volumes of convex bodies”, Proc. 21st ACM Symp. on the Theory of Computing, 1989, pp 375–381.
Feder, T., and Mihail, M., “Balanced Matroids”, Proc. 24th ACM Symp. on the Theory of Computing, 1992, pp. 26–37.
Holzmann, G.J., Design and Validation of Computer Protocols, Prentice Hall Software Series, 1991.
Jerrum, M.R., and Sinclair, A., “Approximating the Permanent”, Proc. 20th ACM Symp. on the Theory of Computing, 1988, pp 235–243.
Lee, D., and Yannakakis, M., “Online minimization of transition systems”, Proc. 24th ACM Symp. on the Theory of Computing, 1992, pp. 264–274.
Mihail, M., “Conductance and Convergence of Markov Chains, A Combinatorial Treatment of Expanders”, Proc. 30th IEEE Symp. on Foundations of Computer Science, 1989.
Reif, J.H., and Smolka, S.A., “The complexity of reachability in distributed communicating processes”, Acta Informatica, Vol. 25, 1988, pp. 333–354.
Rudin, H., “Protocol development success stories: Part 1”, Protocol Specification, Testing, and Verification, XII, Elsevier Science Publishers, (North-Holland), 1992.
West, C.H., “Protocol Validation in Complex Systems”, Proc. 8th ACM Symposium on Principles of Distributed Computing, 1989, pp. 303–312.
Wolper, P., “Specifying interesting properties of programs in propositional temporal logic”, Proc. 13th ACM Symposium on Principles of Programming Languages, 1986, pp. 148–193.
Yannakakis, M., and Lee, D., “Testing Finite State Machines”, Proc. of the 23rd ACM Symp. on the Theory of Computing, 1991, pp. 476–485.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1994 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Mihail, M., Papadimitriou, C.H. (1994). On the random walk method for protocol testing. In: Dill, D.L. (eds) Computer Aided Verification. CAV 1994. Lecture Notes in Computer Science, vol 818. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-58179-0_49
Download citation
DOI: https://doi.org/10.1007/3-540-58179-0_49
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-58179-6
Online ISBN: 978-3-540-48469-1
eBook Packages: Springer Book Archive