Abstract
Formal verification techniques need to deal with the complexity of the systems being verified. Most often, this problem is solved by taking an abstract model of the system and aiming at a complete verification of an approximation of the system. This paper proposes a complementary verification approach, in which the approximation is introduced into the verification algorithm, instead of the system model: we achieve an approximate verification of a fairly complete and detailed system model. The proposed technique relies on coupling a Genetic Algorithm with a simulator of the system under verification, and is especially suited for verifying performance-related aspects. To prove the effectiveness of our approach, we applied it to the quantitative verification of a network protocol: the TCP protocol operating on a given network. A Genetic Algorithm is able to find a configuration of the traffic over the network that sensitizes a critical problem in the TCP protocol that would be difficult to find both with exact techniques and stochastic ones.
Chapter PDF
Similar content being viewed by others
References
E. Alba, J. M. Troya, “Genetic Algorithms for Protocol Validation”, Proceedings of the 4th conference on Parallel Problem Solving (PPSN IV ), Berlin, Germany, September 1996.
K. A. DeJong, “An analysis of the behavior of a class of genetic adaptive systems”, Doctoral Dissertion, University of Michigan, 1975.
J. H. Holland, Adaption in Natural and Artificial Systems, University of Michigan Press, Ann Arbor, MC (USA), 1975.
J. Hui, Switching and Traffic Theory for Integrated Broadband Networks, Kluwer Academic Publishers, 1990.
ISO — Information Processing Systems — Open Systems Interconnection — LOTOS, A Formal Description Technique Based on the Temporal Ordering of Observational Behaviour IS 8807, 1988.
R. J. Linn, Jr., “The features and facilities of ESTELLE”, in Protocol Specification, Testing, and Verification, V. M. Diaz, ed. New York: Elsevier, 1986, pp. 271–296.
B. A. Mah, “INSANE — An Internet Simulated ATM Networking Environment”, available at http://HTTP.CS.Berkeley.EDU/~bmah/Software/Insane/
J. L. Peterson, Petri Net Theory and the Modeling of Systems, Englewood Cliffs, NJ: Prentice-Hall, 1981.
J. Postel. User Datagram Protocol (UDP), RFC 768, August 1980.
J. Postel. Transmission Control Protocol (TCP), RFC 793, Internet Engineering Task Force, January 1981.
R. R. Razouk and C. V. Phelps, “Performance analysis using timed Petri nets”, in Protocol Specification, Testing, and Verification, IV, Y. Yemini, R. Strom, S. Yemini, Eds, New York: Elsevier, 1985, pp. 561–576.
W. R. Stevens, TCP/IP Illustrated: the protocols, Reading, Mass., Addison-Wesley Pub. Co., 1994.
T. Suzuki, S. M. Shatz, and T. Murata, “A Protocol Modeling and Verification Approach Based on a Specification Language and Petri Nets”, IEEE Transactions on Software Engineering, Vol. 16, No. 5, May 1990, pp. 523–536.
L. Wall, T. Christiansen, R. L. Schwartz, Programming Perl, 2nd Edition, O’Reilly, September 1996.
B. B. Welch, Practical Programming in TCL and TK, Prentice Hall Professional Technical Reference, May 1995.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1997 IFIP
About this chapter
Cite this chapter
Baldi, M., Corno, F., Rebaudengo, M., Prinetto, P., Reorda, M.S., Squillero, G. (1997). Simulation-Based Verification of Network Protocols Performance. In: Li, H.F., Probst, D.K. (eds) Advances in Hardware Design and Verification. IFIP Advances in Information and Communication Technology. Springer, Boston, MA. https://doi.org/10.1007/978-0-387-35190-2_16
Download citation
DOI: https://doi.org/10.1007/978-0-387-35190-2_16
Publisher Name: Springer, Boston, MA
Print ISBN: 978-1-5041-2885-8
Online ISBN: 978-0-387-35190-2
eBook Packages: Springer Book Archive