Interprocedural static analysis of sequencing constraints

ABSTRACT

This paper describes a system that automatically performs static interprocedural sequencing analysis from programmable constraint specifications. We describe the algorithms used for interprocedural analysis, relate the problems arising from the analysis of real-world programs, and show how these difficulties were overcome. Finally, we sketch the architecture of our prototype analysis system (called Cesar) and describe our experiences to date with its use, citing performance and error detection characteristics.

REFERENCES

• 1: Krzysztof R. Apt, A Static Analysis of CSP Programs, Proceedings of the Carnegie Mellon Workshop on Logic of Programs, p.1-17, June 06-08, 1983
• 2: ~ARLAZAROV, V. L., DINIC, E. A., KRONROD, M. A., AND FARADZEV, I. A. On economical ~construction of the transitwe closure of a directed graph. Sowet Math. Doklady. 11, 5 (1970) ~1209-1210.
• 3: George S. Avrunin , Ugo A. Buy , James C. Corbett , Laura K. Dillon , Jack C. Wileden, Automated Analysis of Concurrent Systems with the Constrained Expression Toolset, IEEE Transactions on Software Engineering, v.17 n.11, p.1204-1222, November 1991 [doi>10.1109/32.106975]
• 4: G S Avrunin , L K Dillon , J C Wileden , W E Riddle, Constrained expressions: Adding analysis capabilities to design methods for concurrent software systems, IEEE Transactions on Software Engineering, v.12 n.2, p.278-292, Feb. 1986
• 5: G. Bristow , C. Drey , B. Edwards , W. Riddle, Anomaly detection in concurrent programs, Proceedings of the 4th international conference on Software engineering, p.265-273, September 17-19, 1979, Munich, Germany
• 6: E. M. Clarke , E. A. Emerson , A. P. Sistla, Automatic verification of finite-state concurrent systems using temporal logic specifications, ACM Transactions on Programming Languages and Systems (TOPLAS), v.8 n.2, p.244-263, April 1986 [doi>10.1145/5397.5399]
• 7: ~CLEMM, G.M. Persorml communication, Mar. 1988.
• 8: Geoffrey Clemm , Leon Osterweil, A mechanism for environment integration, ACM Transactions on Programming Languages and Systems (TOPLAS), v.12 n.1, p.1-25, Jan. 1990 [doi>10.1145/77606.77607]
• 9: Laura K. Dillon , George S. Avrunin , Jack C. Wileden, Constrained expressions: toward broad applicability of analysis methods for distributed software systems, ACM Transactions on Programming Languages and Systems (TOPLAS), v.10 n.3, p.374-402, July 1988 [doi>10.1145/44501.44502]
• 10: Bo Einarsson , W. Morven Gentleman, Mixed language programming, Software—Practice & Experience, v.14 n.4, p.383-392, April 1984 [doi>10.1002/spe.4380140410]
• 11: P. Fairfield , M. A. Hennell, Data flow analysis of recursive procedures, ACM SIGPLAN Notices, v.23 n.1, p.48-57, Jan., 1988 [doi>10.1145/44304.44308]
• 12: ~FELDM^N, S. h Make--a program for maintaining computer programs Softw. Pract. Exper. ~9.4 (Apr 1979), 255-265
• 13: ~FOSDICK, L. D., AND OSTERWEIL, L. J DAVE--a validation, error detection and documenta- ~tion system for FORTRAN programs Softw. Pract. Exper. 6, 4 (Sept. 1976), 473-486.
• 14: ~FREUD~NBE}mER, S. M. On the use of global optimization algorithms for the detection of ~semantic programming errors. PhD thesis, Courant Inst., New York Univ., 1984
• 15: John V. Guttag , Ellis Horowitz , David R. Musser, Abstract data types and software validation, Communications of the ACM, v.21 n.12, p.1048-1064, Dec. 1978 [doi>10.1145/359657.359666]
• 16: ~HOWDEN, W E A general model for static analysis. In Procee&ngs of the 16th Hawatt ~International Conference on System Sctences (Honolulu, Jan. 1983), pp. 163 169.
• 17: W E Howden, A functional approach to program testing and analysis, IEEE Transactions on Software Engineering, v.12 n.10, p.997-1005, Oct. 1986
• 18: William E Howden, Functional program testing and analysis, McGraw-Hill, Inc., New York, NY, 1986
• 19: W. Howden, Validating programs without specifications, Proceedings of the ACM SIGSOFT '89 third symposium on Software testing, analysis, and verification, p.2-9, December 13-15, 1989, Key West, Florida, United States
• 20: William E. Howden, Comments Analysis and Programming Errors, IEEE Transactions on Software Engineering, v.16 n.1, p.72-81, January 1990 [doi>10.1109/32.44365]
• 21: ~LUCK~^M, D. C., HELMBOLD, D. P., MELDAL, S., BR~^N, D. L, AND HAB~RLER, M A Task ~sequencing language for specifying distributed Ada systems (TSL-1). Tech. Rep CSL-TR-87- ~334, Computer Systems Laboratory, Stanford Univ., July 1987
• 22: Kurt M. Olender , Leon J. Osterweil, Cecil: A Sequencing Constraint Language for Automatic Static Analysis Generation, IEEE Transactions on Software Engineering, v.16 n.3, p.268-280, March 1990 [doi>10.1109/32.48935]
• 23: ~OSTERWEn,, L. J Toolpack--an experimental software development enwronment research ~project. IEEE Trans. Softw. Eng. SE-9, 11 (Nov. 1983), 673 685
• 24: ~SHARm, M., ANI~ PNEULI, A Two approaches to interprocedural data flow analysis. In ~Program Flow Analysis. S S. Muchnick and N. D. Jones, Eds. Prentice-Hall, Englewood ~Cliffs, N.J., 1981, pp. 189-233.
• 25: R E Strom , S Yemini, Typestate: A programming language concept for enhancing software reliability, IEEE Transactions on Software Engineering, v.12 n.1, p.157-171, Jan. 1986
• 26: Robert Endre Tarjan, Fast Algorithms for Solving Path Problems, Journal of the ACM (JACM), v.28 n.3, p.594-614, July 1981 [doi>10.1145/322261.322273]
• 27: Richard N. Taylor, A general-purpose algorithm for analyzing concurrent programs, Communications of the ACM, v.26 n.5, p.361-376, May 1983 [doi>10.1145/69586.69587]
• 28: ~TAYLOR, R N., AND OSTERWEIL, L J Anomaly detection in concurrent software by static ~data flow analysis. IEEE Trans. on Softw. Eng. SE-6 (May 1980), 265-277.
• 29: ~WEISER, M. Program slicing IEEE Trans Softw. Eng. SE-IO, 4 (July 1984), 352-357
• 30: ~WERNER, L L, ^~D HOWDEN, W E Fault detection in COBOL programs by means of data ~usage analysis. Tech. Rep. CS-87-111. Dept. of Computer Science, Umv. of California, San ~Diego, Dec 1987.
• 31: Cindy Wilson , Leon J. Osterweil, Omega—a data flow analysis tool for the C programming language, IEEE Transactions on Software Engineering, v.11 n.9, p.832-838, Sept. 1985 [doi>10.1109/TSE.1985.232542]
• 32: ~YOUNG, M, AND TAYLOR, R. N. Combining static concurrency analysis with symbolic ~execution. In Procee&ngs of the Workshop on Software Testing (Banff, Alberta, July 15-17, ~1986), pp. 170-180
• 33: M. Young , R. Taylor , K. Forester , D. Brodbeck, Integrated concurrency analysis in a software development enviornment, Proceedings of the ACM SIGSOFT '89 third symposium on Software testing, analysis, and verification, p.200-209, December 13-15, 1989, Key West, Florida, United States

INDEX TERMS

Primary Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.1 Requirements/Specifications
          Subjects: Languages

Additional Classification:
  D. Software
  D.1 PROGRAMMING TECHNIQUES
  D.2 SOFTWARE ENGINEERING
      D.2.1 Requirements/Specifications
          Subjects: Methodologies (e.g., object-oriented, structured)
      D.2.2 Design Tools and Techniques
          Subjects: Computer-aided software engineering (CASE)
      D.2.4 Software/Program Verification
          Subjects: Validation; Reliability
      D.2.5 Testing and Debugging
          Subjects: Debugging aids

General Terms:
Algorithms, Languages, Reliability, Verification

Keywords:
error detection, interprocedural data flow analysis, sequencing constraints