Applications of feasible path analysis to program testing

ABSTRACT

For certain structural testing criteria a significant proportion of tests instances are infeasible in the sense the semantics of the program implies that test data cannot be constructed that meet the test requirement. This paper describes the design and prototype implementation of a structural testing system that uses a theorem prover to determine feasibility of testing requirements and to optimize the number of test cases required to achieve test coverage. Using this approach, we were able to accurately and efficiently determine path feasibility for moderately-sized program units of production code written in a subset of Ada. On these problems, the computer solutions were obtained much faster and with greater accuracy than manual analysis. The paper describes how we formalize test criteria as control flow graph path expressions; how the criteria are mapped to logic formulas; and how we control the complexity of the inference task. It describes the limitations of the system and proposals for its improvement as well as other applications of the analysis.

REFERENCES

• Andrews81: Peter B. Andrews, Theorem Proving via General Matings, Journal of the ACM (JACM), v.28 n.2, p.193-214, April 1981 [doi>10.1145/322248.322249]
• Bibel81: Wolfgang Bibel, On Matrices with Connections, Journal of the ACM (JACM), v.28 n.4, p.633-645, Oct. 1981 [doi>10.1145/322276.322277]
• Bicevskis79: Bicevskis, J., Borzovs, J., Straujums, U., Zarins, A., and Miller, E. SMOTL -- a system to construct samples for data processing program debugging. IEEE Transactions on Software Engineering SE-5, 8 (August 1990), 60-- 66.
• Bledsoe83: Bledsoe, W. W. The UT interactive prover. Tech. Report ATP- 17B, Department of Mathematics, The University of Texas at Austin (1983).
• Boyer75: Robert S. Boyer , Bernard Elspas , Karl N. Levitt, SELECT—a formal system for testing and debugging programs by symbolic execution, ACM SIGPLAN Notices, v.10 n.6, p.234-245, June 1975
• Boyer86: R. S. Boyer , J. S. Moore, Integrating decision procedures into heuristic theorem provers: a case study of linear arithmetic, Machine intelligence 11, Oxford University Press, Inc., New York, NY, 1988
• Clarke76: Clarke, L.A. A system to generate test data and symbolically execute programs. IEEE Transactions on Software Engineering SE-2, 3 (September 1976), 215--222.
• Clarke88: Lori A. Clarke , Debra J. Richardson , Steven J. Zeil, TEAM: a support environment for testing, evaluation, and analysis, Proceedings of the third ACM SIGSOFT/SIGPLAN software engineering symposium on Practical software development environments, p.153-162, November 28-30, 1988, Boston, Massachusetts, United States
• Field93: Field, J., A simple rewriting semantics for realistic imperative programs and its application to program analysis, Revision of paper appearing in the 1992 Workshop on Partial Evaluation and Semantics-Based Program Manipulation, San Francisco.
• Frankl88: P. G. Frankl , E. J. Weyuker, An Applicable Family of Data Flow Testing Criteria, IEEE Transactions on Software Engineering, v.14 n.10, p.1483-1498, October 1988 [doi>10.1109/32.6194]
• Goff91: Gina Goff , Ken Kennedy , Chau-Wen Tseng, Practical dependence testing, Proceedings of the ACM SIGPLAN 1991 conference on Programming language design and implementation, p.15-29, June 24-28, 1991, Toronto, Ontario, Canada
• Hoare69: C. A. R. Hoare, An axiomatic basis for computer programming, Communications of the ACM, v.12 n.10, p.576-580, Oct. 1969 [doi>10.1145/363235.363259]
• Horwitz88: S. Horwitz , J. Prins , T. Reps, On the adequacy of program dependence graphs for representing programs, Proceedings of the 15th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.146-157, January 10-13, 1988, San Diego, California, United States [doi>10.1145/73560.73573]
• Howden77: Howden, W.E. Symbolic testing and the DISSECT symbolic evaluation techniques. IEEE Transactions on Software Engineering SE-4, 4 (1977), 266--278.
• Jasper94: Robert Jasper , Mike Brennan , Keith Williamson , Bill Currier , David Zimmerman, Test data generation and feasible path analysis, Proceedings of the 1994 ACM SIGSOFT international symposium on Software testing and analysis, p.95-107, August 17-19, 1994, Seattle, Washington, United States [doi>10.1145/186258.187150]
• Korel90: B. Korel, Automated Software Test Data Generation, IEEE Transactions on Software Engineering, v.16 n.8, p.870-879, August 1990 [doi>10.1109/32.57624]
• Kotik89: G. Kotik , L. Markosian, Automating software analysis and testing using a program transformation system, Proceedings of the ACM SIGSOFT '89 third symposium on Software testing, analysis, and verification, p.75-84, December 13-15, 1989, Key West, Florida, United States
• Laski90: J. Laski, Data flow testing in STAD, Journal of Systems and Software, v.12 n.1, p.3-14, Apr. 1990 [doi>10.1016/0164-1212(90)90062-Q]
• Letovsky88: Stanley Ian Letovsky, Plan analysis of programs, 1988
• Murray87: Neil V. Murray , Erik Rosenthal, Inference with path resolution and semantic graphs, Journal of the ACM (JACM), v.34 n.2, p.225-254, April 1987 [doi>10.1145/23005.23716]
• Pugh92: William Pugh, A practical algorithm for exact array dependence analysis, Communications of the ACM, v.35 n.8, p.102-114, Aug. 1992 [doi>10.1145/135226.135233]
• Ramamoorthy76: Ramamoorthy, C., Ho, S., and Chen, W. On the automated generation of program test data. IEEE Transactions on Software Engineering SE- 2, 4 (December 1976), 293--300.
• Reasoning90: RefineTM 3.0 User's Guide, Reasoning Systems Incorporated, Palo Alto, CA. May 25 1990.
• Reasoning92: Refine/Ada User's Guide, Reasoning Systems incorporated, Palo Alto, CA. July 26, 1992.
• Shostak79: Robert E. Shostak, A Practical Decision Procedure for Arithmetic with Function Symbols, Journal of the ACM (JACM), v.26 n.2, p.351-360, April 1979 [doi>10.1145/322123.322137]
• Shostak81: Robert Shostak, Deciding Linear Inequalities by Computing Loop Residues, Journal of the ACM (JACM), v.28 n.4, p.769-779, Oct. 1981 [doi>10.1145/322276.322288]
• Shostak84: Robert E. Shostak, Deciding Combinations of Theories, Journal of the ACM (JACM), v.31 n.1, p.1-12, Jan. 1984 [doi>10.1145/2422.322411]
• Smith90: D. R. Smith, KIDS: A Semiautomatic Program Development System, IEEE Transactions on Software Engineering, v.16 n.9, p.1024-1043, September 1990 [doi>10.1109/32.58788]
• Tripathy91: Piyu Tripathy , Behcet Sarikaya, Test Generation from LOTOS Specifications, IEEE Transactions on Computers, v.40 n.4, p.543-552, April 1991 [doi>10.1109/12.88472]
• Wang85: Wang, T.C. Designing examples for semantically guided hierarchical deduction. In 9th International Joint Conference on Artificial Intelligence (Los Angeles, California, August 18-23, 1985).
• Wang87: Tie-Cheng Wang , W. W. Bledsoe, Hierarchical deduction, Journal of Automated Reasoning, v.3 n.1, p.35-77, March 1987 [doi>10.1007/BF00381144]
• Wang92: Tie-Cheng Wang , Allen Goldberg, RVF: An Automated Formal Verification System, Proceedings of the 11th International Conference on Automated Deduction: Automated Deduction, p.735-739, June 15-18, 1992
• Werner91: Linda L. Werner , William E. Howden, An investigation of the applicability of data usage analysis, Journal of Systems and Software, v.15 n.3, p.205-215, July 1991 [doi>10.1016/0164-1212(91)90037-7]
• Weyuker88: Weyuker, E.J. An empirical study of the complexity of data flow testing. In Proceedings of the Second Workshop on Software Testing, Analysis, and Verification, Banff, Canada, July 19-- 21, 1988, IEEE Computer Society, pp. 188--195.
• Weyuker90: Elaine J. Weyuker, The Cost of Data Flow Testing: An Empirical Study, IEEE Transactions on Software Engineering, v.16 n.2, p.121-128, February 1990 [doi>10.1109/32.44376]
• Wills87: Linda M. Wills, Automated Program Recognition, Massachusetts Institute of Technology, Cambridge, MA, 1987
• Woodward80: Woodward, M.R., Hedley, D., and Hennell, M.A. Experience with path analysis and testing. In Tutorial: Software Testing & Validation Techniques, 2Ed, E.Miller and W. Howden, Eds. IEEE Computer Society Press, Los Alamitos, CA, 1981, pp. 194--206.
• Wos68: Wos, L., and Robinson, A, Paramodulation and set of support. Proceedings of the IRIA Symposium on Automatic Demonstration, Versailles, France, France, Spring-Verlag (1968) 276-310.
• Yates89: D. Yates , N. Malevris, Reducing the effects of infeasible paths in branch testing, Proceedings of the ACM SIGSOFT '89 third symposium on Software testing, analysis, and verification, p.48-54, December 13-15, 1989, Key West, Florida, United States

INDEX TERMS

Primary Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.5 Testing and Debugging
          Subjects: Testing tools (e.g., data generators, coverage testing)

Additional Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.2 Language Classifications

          Nouns: Ada
      D.3.3 Language Constructs and Features
          Subjects: Control structures; Data types and structures

  F. Theory of Computation
  F.2 ANALYSIS OF ALGORITHMS AND PROBLEM COMPLEXITY
      F.2.2 Nonnumerical Algorithms and Problems
          Subjects: Computations on discrete structures
  F.4 MATHEMATICAL LOGIC AND FORMAL LANGUAGES
      F.4.1 Mathematical Logic
          Subjects: Mechanical theorem proving

General Terms:
Design, Languages, Reliability, Theory