Software assurance by bounded exhaustive testing

ABSTRACT

The contribution of this paper is an experiment that shows the potential value of a combination of selective reverse engineering to formal specifications and bounded exhaustive testing to improve the assurance levels of complex software. A key problem is to scale up test input generation so that meaningful results can be obtained. We present an approach, using Alloy and TestEra for test input generation, which we evaluate by experimental application to the Galileo dynamic fault tree analysis tool.

REFERENCES

• 1: Bayardo, R. J. Jr. and Schrag, R. C. Using CSP look-back techniques to solve real-world SAT instances. In Proceedings of the 14th National Conference on Artificial Intelligence and 9th Innovative Applications of Artificial Intelligence Conference (AAAI-97/IAAI-97), pages 203--208, Menlo Park, July 27-31 1997. AAAI Press.
• 2: Boris Beizer, Software testing techniques (2nd ed.), Van Nostrand Reinhold Co., New York, NY, 1990
• 3: Chandrasekhar Boyapati , Sarfraz Khurshid , Darko Marinov, Korat: automated testing based on Java predicates, Proceedings of the 2002 ACM SIGSOFT international symposium on Software testing and analysis, July 22-24, 2002, Roma, Italy
• 4: Mark Allen Boyd, Dynamic fault tree models: techniques for analysis of advanced fault tolerant computer systems, Duke University, Durham, NC, 1992
• 5: Juei Chang , Debra J. Richardson, Structural specification-based testing: automated support and experimental evaluation, Proceedings of the 7th European software engineering conference held jointly with the 7th ACM SIGSOFT international symposium on Foundations of software engineering, p.285-302, September 06-10, 1999, Toulouse, France
• 6: Chilenski, J. J., and Miller, S. P. Applicability of modified condition/decision coverage to software testing. Software Engineering Journal, 9(5):191--200.
• 7: David Coppit , Robert R. Painter , Kevin J. Sullivan, Shared Semantic Domains for Computational Reliability Engineering, Proceedings of the 14th International Symposium on Software Reliability Engineering, p.169, November 17-21, 2003
• 8: David Coppit , Kevin J. Sullivan, Galileo: a tool built from mass-market applications, Proceedings of the 22nd international conference on Software engineering, p.750-753, June 04-11, 2000, Limerick, Ireland [doi>10.1145/337180.337622]
• 9: David Wayne Coppit , Kevin J. Sullivan, Engineering modeling and analysis: sound methods and effective tools, 2003
• 10: David Coppit , Kevin J. Sullivan, Sound methods and effective tools for engineering modeling and analysis, Proceedings of the 25th International Conference on Software Engineering, May 03-10, 2003, Portland, Oregon
• 11: David Coppit , Kevin J. Sullivan , Joanne Bechta Dugan, Formal Semantics for Computational Engineering: A Case Study on Dynamic Fault Trees, Proceedings of the 11th International Symposium on Software Reliability Engineering (ISSRE'00), p.270, October 08-11, 2000
• 12: Jeremy Dick , Alain Faivre, Automating the Generation and Sequencing of Test Cases from Model-Based Specifications, Proceedings of the First International Symposium of Formal Methods Europe on Industrial-Strength Formal Methods, p.268-284, April 19-23, 1993
• 13: Stacy A. Doyle, Dependability Assessment Using Binary Decision Diagrams (BDDs), Proceedings of the Twenty-Fifth International Symposium on Fault-Tolerant Computing, p.249, June 27-30, 1995
• 14: Dugan, J. B., Bavuso, S., and Boyd, M. Dynamic fault-tree models for fault-tolerant computer systems. IEEE Transactions on Reliability, 41(3):363--77, Sept. 1992.
• 15: Dugan, J. B., Sullivan, K. J., and Coppit, D. Developing a low-cost high-quality software tool for dynamic fault tree analysis. In IEEE Transactions on Reliability, December 1999.
• 16: Dugan, J. B., Venkataraman, B., and Gulati, R. DIFTree: A software package for the analysis of dynamic fault tree models. In Annual Reliability and Maintainability Symposium 1997 Proceedings, Philadelphia, PA, January 1997.
• 17: Marc Fisher , Mingming Cao , Gregg Rothermel , Curtis R. Cook , Margaret M. Burnett, Automated test case generation for spreadsheets, Proceedings of the 24th International Conference on Software Engineering, May 19-25, 2002, Orlando, Florida [doi>10.1145/581339.581359]
• 18: Patrice Godefroid, Model checking for programming languages using VeriSoft, Proceedings of the 24th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.174-186, January 15-17, 1997, Paris, France [doi>10.1145/263699.263717]
• 19: Mary Jean Harrold, Testing: a roadmap, Proceedings of the Conference on The Future of Software Engineering, p.61-72, June 04-11, 2000, Limerick, Ireland [doi>10.1145/336512.336532]
• 20: Havelund, K. and Pressburger, T. Model checking Java programs using Java PathFinder. International Journal on Software Tools for Technology Transfer, 1999.
• 21: Steffen Helke , Thomas Neustupny , Thomas Santen, Automating Test Case Generation from Z Specifications with Isabelle, Proceedings of the 10th International Conference of Z Users on The Z Formal Specification Notation, p.52-71, April 03-04, 1997
• 22: Hans-Martin Hörcher, Improving Software Tests Using Z Specifications, Proceedings of the 9th International Conference of Z Usres on The Z Formal Specification Notation, p.152-166, September 07-09, 1995
• 23: Jackson, D. Micromodels of software: Modelling and analysis with Alloy. 2001. http://sdg.lcs.mit.edu/alloy/reference-man-ual. pdf
• 24: Daniel Jackson , Ian Schechter , Hya Shlyahter, Alcoa: the alloy constraint analyzer, Proceedings of the 22nd international conference on Software engineering, p.730-733, June 04-11, 2000, Limerick, Ireland [doi>10.1145/337180.337616]
• 25: Khurshid, S., Marinov, D., Shlyakhter, I., Jackson, D. A Case for Efficient Solution Enumeration. Sixth International Conference on Theory and Applications of Satisfiability Testing (SAT 2003), S. Margherita Ligure - Portofino (Italy), May 2003.
• 26: Khurshid, S., and Marinov, D. "Checking a Java implementation of a naming architecture using TestEra," In Post-CAV Workshop on Software Model Checking, volume 55(3) of Electronic Notes in Theoretical Computer Science (ENTCS), Paris, France, July 2001. Elsevier Science.
• 27: Khurshid, S., and Pasareanu, C., "Generalized symbolic execution for model checking and testing, " 9th International Conference on Tools and Algorithms for Construction and Analysis of Systems (TACAS), Warsaw, Poland, April, 2003.
• 28: James C. King, Symbolic execution and program testing, Communications of the ACM, v.19 n.7, p.385-394, July 1976 [doi>10.1145/360248.360252]
• 29: J. C. Knight , N. G. Leveson, An experimental evaluation of the assumption of independence in multiversion programming, IEEE Transactions on Software Engineering, v.12 n.1, p.96-109, Jan. 1986
• 30: Lions, J.L., Ariane 5: Flight 501 Failure, Report by the Inquiry Board, Paris, 1996.
• 31: MacColl, I., Carrington, D., and Stocks, P. An Experiment in Specification-based Testing. Technical Report No. 96-05, Software Verification Research Centre, Department of Computer Science, The University of Queensland. May 1996.
• 32: Darko Marinov , Sarfraz Khurshid, TestEra: A Novel Framework for Automated Testing of Java Programs, Proceedings of the 16th IEEE international conference on Automated software engineering, p.22, November 26-29, 2001
• 33: Marinov, D., A. Andoni, D. Daniliuc, S. Khurshid, and M. Rinard, "An evaluation of exhaustive testing for data structures," MIT Computer Science and Artificial Intelligence Laboratory Report MIT -LCS-TR-921, September, 2003.
• 34: Matthew W. Moskewicz , Conor F. Madigan , Ying Zhao , Lintao Zhang , Sharad Malik, Chaff: engineering an efficient SAT solver, Proceedings of the 38th conference on Design automation, p.530-535, June 2001, Las Vegas, Nevada, United States [doi>10.1145/378239.379017]
• 35: Offutt, J., and Abdurazik, A. Generating Test from UML Specifications. In UML conference proceedings, Fort Collins, CO, October 1999.
• 36: Sandra Rapps , Elaine J. Weyuker, Selecting software test data using data flow information, IEEE Transactions on Software Engineering, v.11 n.4, p.367-375, April 1985 [doi>10.1109/TSE.1985.232226]
• 37: Mark Saaltink, The Z/EVES System, Proceedings of the 10th International Conference of Z Users on The Z Formal Specification Notation, p.72-85, April 03-04, 1997
• 38: Schwartz, E. Design and implementation of intentional names. Master's thesis, MIT Laboratory for Computer Science, Cambridge, MA, June 1999.
• 39: Shlyakhter, L. Generating effective symmetry-breaking predicates for search problems. In Proc. Workshop on Theory and Applications of Satisfiability Testing. June 2001.
• 40: J. M. Spivey, The Z notation: a reference manual, Prentice Hall International (UK) Ltd., Hertfordshire, UK, 1992
• 41: Phil Stocks , David Carrington, A Framework for Specification-Based Testing, IEEE Transactions on Software Engineering, v.22 n.11, p.777-793, November 1996 [doi>10.1109/32.553698]
• 42: Kevin J. Sullivan , Joanne Bechta Dugan , David Coppit, The Galileo Fault Tree Analysis Tool, Proceedings of the Twenty-Ninth Annual International Symposium on Fault-Tolerant Computing, p.232, June 15-18, 1999
• 43: Sun Microsystems. Java 2 Platform, Standard Edition, v1.3.1 API Specification. http://java.sun.com/j2se/1.3/docs/api/
• 44: Vesely, W. E., Goldberg, F. F., Roberts, N. H., and Haasl, D. F. Fault Tree Handbook. U. S. Nuclear Regulatory Commission, NUREG-0492, Washington DC, 1981.
• 45: Weyuker, E. J., and Ostrand, T. J. Theories of program testing and the the application of revealing subdomains. IEEE Transactions on Software Engineering, 6(3):236--246, May 1980.

INDEX TERMS

Primary Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.4 Software/Program Verification

Additional Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.5 Testing and Debugging

General Terms:
Experimentation, Reliability, Verification

Keywords:
TestEra, automated test case generation, bounded exhaustive testing, formal methods, reverse engineering, specification-based testing