Using production grammars in software testing

ABSTRACT

Extensible typesafe systems, such as Java, rely critically on a large and complex software base for their overall protection and integrity, and are therefore difficult to test and verify. Traditional testing techniques, such as manual test generation and formal verification, are too time consuming, expensive, and imprecise, or work only on abstract models of the implementation and are too simplistic. Consequently, commercial virtual machines deployed so far have exhibited numerous bugs and security holes.In this paper, we discuss our experience with using production grammars in testing large, complex and safety-critical software systems. Specifically, we describe lava, a domain specific language we have developed for specifying production grammars, and relate our experience with using lava to generate effective test suites for the Java virtual machine. We demonstrate the effectiveness of production grammars in generating complex test cases that can, when combined with comparative and variant testing techniques, achieve high code and value coverage. We also describe an extension to production grammars that enables concurrent generation of certificates for test cases. A certificate is a behavioral description that specifies the intended outcome of the generated test case, and therefore acts as an oracle by which the correctness of the tested system can be evaluated in isolation. We report the results of applying these testing techniques to commercial Java implementations. We conclude that the use of production grammars in combination with other automated testing techniques is a powerful and effective method for testing software systems, and is enabled by a special purpose language for specifying extended production grammars.

REFERENCES

• Adl-Tabatabai et al. 96: Ali-Reza Adl-Tabatabai , Geoff Langdale , Steven Lucco , Robert Wahbe, Efficient and language-independent mobile programs, Proceedings of the ACM SIGPLAN 1996 conference on Programming language design and implementation, p.127-136, May 21-24, 1996, Philadelphia, Pennsylvania, United States
• Aho et al 88: Alfred V. Aho , Brian W. Kernighan , Peter J. Weinberger, The AWK programming language, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 1987
• Bauer&Lamb 79: Jonathan A. Bauer , Alan B. Finger, Test plan generation using formal grammars, Proceedings of the 4th international conference on Software engineering, p.425-432, September 17-19, 1979, Munich, Germany
• Berners-Lee et al 96: Berners-Lee, T., Fielding, R., Frystyk, H. "Informational RFC 1945 - Hypertext Transfer Protocol -- HTTP/1.0," Request for Comments, Internet Engineering Task Force, May 1996.
• Celentano et al. 80: Celentano, A., Crespi-Reghizzi, S., Vigna, P. D., Ghezzi, C., Granata, G., and Savoretti, F. "Compiler Testing Using a Sentence Generator." In Software: Practice ~ Experience. 10(11), 1980, pp. 897-918.
• Chang et al. 95: Chang, J., Richardson, D. J., and Sankar, S. "Automated Test Selection from ADL Speciflcattons." In the First California Software Symposium (CSS'95), March 1995.
• Dean et al. 97: Drew Dean , Edward W. Felten , Dan S. Wallach , Dirk Balfanz, Java security: Web browsers and beyond, Internet besieged: countering cyberspace scofflaws, ACM Press/Addison-Wesley Publishing Co., New York, NY, 1997
• Dershowitz & Jouannaud 90: Nachum Dershowitz , Jean-Pierre Jouannaud, Rewrite systems, Handbook of theoretical computer science (vol. B): formal models and semantics, MIT Press, Cambridge, MA, 1991
• Dershowitz 93: Nachum Dershowitz, A Taste of Rewrite Systems, Functional Programming, Concurrency, Simulation and Automated Reasoning: International Lecture Series 1991-1992, McMaster University, Hamilton, Ontario, Canada, p.199-228, January 1993
• Drossopoulou & Eisenbach 97: Drossopoulou, S., Elsenbach, S. "Java Is Typesafe - Probably." In 11th European Conference on Object Oriented Programming, June 1997.
• Drossopoulou & Eisenbach 98: Drossopoulou, S., Eisenbach, S. "Towards an Operational Semantics and Proof of Type Soundness for Java." March 1998, to be published, http://www-dse.doc.ic.ac.uk/projects/slurp/ pubs/chapter.ps.
• Drossopoulou et al. 99: Sophia Drossopoulou , Susan Eisenbach , Sarfraz Khurshid, Is the Java type system sound?, Theory and Practice of Object Systems, v.5 n.1, p.3-24, Jan. 1999 [doi>10.1002/(SICI)1096-9942(199901/03)5:1<3::AID-TAPO2>3.0.CO;2-T ]
• Freund&Mitchell 98: Stephen N. Freund , John C. Mitchell, A type system for object initialization in the Java bytecode language, Proceedings of the 13th ACM SIGPLAN conference on Object-oriented programming, systems, languages, and applications, p.310-327, October 18-22, 1998, Vancouver, British Columbia, Canada
• Freund&Mitchell 99: Freund, S. N. and Mitchell, J. C. "A Type System for Java Bytecode Subroutines and Exceptions." To be published.
• Gargantini & Heitmeyer 99: Angelo Gargantini , Constance Heitmeyer, Using model checking to generate tests from requirements specifications, Proceedings of the 7th European software engineering conference held jointly with the 7th ACM SIGSOFT international symposium on Foundations of software engineering, p.146-162, September 06-10, 1999, Toulouse, France
• Griswold: Griswold, D. "The Java HotSpot Virtual Machine Architecture." http://www.javasoft.com/ products/hotspot/whitepaper.html
• Inferno: Lucent Technologies. Inferno. http://inferno.bell-labs.com/mferno/
• Lindholm&Yellin 99: Tim Lindholm , Frank Yellin, Java Virtual Machine Specification, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 1999
• Mandrioli et al. 95: Dino Mandrioli , Sandro Morasca , Angelo Morzenti, Generating test cases for real-time systems from logic specifications, ACM Transactions on Computer Systems (TOCS), v.13 n.4, p.365-398, Nov. 1995 [doi>10.1145/210223.210226]
• McGraw & Felten 96: Gary McGraw , Edward W. Felten, Java security: hostile applets, holes&antidotes, John Wiley & Sons, Inc., New York, NY, 1997
• McKeeman 98: McKeeman, W. M. "Differential Testing for Software." Digital Technical Journal Vol 10, No 1, December 1998.
• Meyer & Downing 97: Jon Meyer , Troy Downing, Java virtual machine, O'Reilly & Associates, Inc., Sebastopol, CA, 1997
• Muller et al. 97: Muller, G., Moura, B., Bellard, F., Consel, C. "Harissa: A Flexible and Efficient Java Environment Mixing Bytecode and Compiled Code." In Proceedings of the Third Conference on Object Oriented Technologies, 1997.
• Necula 97: George C. Necula, Proof-carrying code, Proceedings of the 24th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.106-119, January 15-17, 1997, Paris, France [doi>10.1145/263699.263712]
• Necula & Lee 98: George C. Necula , Peter Lee, The design and implementation of a certifying compiler, Proceedings of the ACM SIGPLAN 1998 conference on Programming language design and implementation, p.333-344, June 17-19, 1998, Montreal, Quebec, Canada
• Oracle: Oracle Corporation. Oracle Application Server Release 4.0 Documentation. http://technet.oracle.com/ doc/was.htm
• Proebsting et al. 97: Proebstmg, T. A., Townsend, G., Bridges, P., Hartman, J.H., Newsham, T. and Watterson S. A. "Toba: Java for Applications: A Way Ahead of Time (WAT) Compiler." In Proceedings of the Third Conference on Object Oriented Technologies, 1997.
• Prusinkiewicz et al. 88: Przemyslaw Prusinkiewicz , Aristid Lindenmayer , James Hanan, Development models of herbaceous plants for computer imagery purposes, ACM SIGGRAPH Computer Graphics, v.22 n.4, p.141-150, Aug. 1988
• Sirer et al. 98: Emin Gün Sirer , Robert Grimm , Brian N. Bershad , Arthur J. Gregory , Sean McDirmid, Distributed virtual machines: a system architecture for network computing, Proceedings of the 8th ACM SIGOPS European workshop on Support for composing distributed applications, p.13-16, September 1998, Sintra, Portugal [doi>10.1145/319195.319198]
• Stata&Abadi 98: Raymie Stata , Martín Abadi, A type system for Java bytecode subroutines, Proceedings of the 25th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.149-160, January 19-21, 1998, San Diego, California, United States [doi>10.1145/268946.268959]
• SunJWS: Sun. Java Web Server. http://www.sun.com/ so ftware/iwebserver/index .html
• Syme 97: Syme, D. "Proving Java Type-Soundness." University of Cambridge Computer Laboratory Technical Report 427, June 1997.
• Weyuker et al. 94: E. Weyuker , T. Goradia , A. Singh, Automatically Generating Test Data from a Boolean Specification, IEEE Transactions on Software Engineering, v.20 n.5, p.353-363, May 1994 [doi>10.1109/32.286420 ]

INDEX TERMS

Primary Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING

Additional Classification:
  F. Theory of Computation
  F.4 MATHEMATICAL LOGIC AND FORMAL LANGUAGES

General Terms:
Experimentation, Verification