Residual dynamic typestate analysis exploiting static analysis: results to reformulate and reduce the cost of dynamic analysis

ABSTRACT

Programmers using complex libraries and frameworks are faced with the difficult task of ensuring that their implementations comply with complex and informally described rules for proper sequencing of API calls. Recent advances in static and dynamic techniques for checking explicit specifications of program typestate properties have shown promise in addressing this challenge. Unfortunately, static typestate analyses are limited in their scalability and dynamic analyses can suffer from significant run-time overhead. In this paper, we present an approach that exploits information calculated by flow-sensitive static typestate analyses to reformulate the original analysis problem as a residual dynamic typestate analysis. We demonstrate that residual analyses retain the error reporting of unoptimized dynamic analysis while offering the potential for significantly reducing analysis cost

REFERENCES

• 1: Hira Agrawal, Efficient coverage testing using global dominator graphs, Proceedings of the 1999 ACM SIGPLAN-SIGSOFT workshop on Program analysis for software tools and engineering, p.11-20, September 06-06, 1999, Toulouse, France
• 2: Matthew Arnold , Barbara G. Ryder, A framework for reducing the cost of instrumented code, Proceedings of the ACM SIGPLAN 2001 conference on Programming language design and implementation, p.168-179, June 2001, Snowbird, Utah, United States
• 3: E. Bodden, L. Hendren, and O. Lhotak. A staged static program analysis to improve the performance of runtime monitoring. In 21st Euro. Conf. on Obj.-Oriented Prog., 2007.
• 4: Rastislav Bodík , Rajiv Gupta , Vivek Sarkar, ABCD: eliminating array bounds checks on demand, Proceedings of the ACM SIGPLAN 2000 conference on Programming language design and implementation, p.321-333, June 18-21, 2000, Vancouver, British Columbia, Canada
• 5: Marcelo d'Amorim , Klaus Havelund, Event-based runtime verification of java programs, Proceedings of the third international workshop on Dynamic analysis, p.1-7, May 17-17, 2005, St. Louis, Missouri
• 6: Nurit Dor , Stephen Adams , Manuvir Das , Zhe Yang, Software validation via scalable path-sensitive value flow analysis, Proceedings of the 2004 ACM SIGSOFT international symposium on Software testing and analysis, July 11-14, 2004, Boston, Massachusetts, USA
• 7: Matthew B. Dwyer , George S. Avrunin , James C. Corbett, Patterns in property specifications for finite-state verification, Proceedings of the 21st international conference on Software engineering, p.411-420, May 16-22, 1999, Los Angeles, California, United States [doi>10.1145/302405.302672]
• 8: Matthew B. Dwyer , Alex Kinneer , Sebastian Elbaum, Adaptive Online Program Analysis, Proceedings of the 29th international conference on Software Engineering, p.220-229, May 20-26, 2007 [doi>10.1109/ICSE.2007.12]
• 9: Matthew B. Dwyer , Lori A. Clarke , Jamieson M. Cobleigh , Gleb Naumovich, Flow analysis for verifying properties of concurrent software systems, ACM Transactions on Software Engineering and Methodology (TOSEM), v.13 n.4, p.359-430, October 2004 [doi>10.1145/1040291.1040292]
• 10: Stephen Fink , Eran Yahav , Nurit Dor , G. Ramalingam , Emmanuel Geay, Effective typestate verification in the presence of aliasing, Proceedings of the 2006 international symposium on Software testing and analysis, July 17-20, 2006, Portland, Maine, USA [doi>10.1145/1146238.1146254]
• 11: Cormac Flanagan, Hybrid type checking, Conference record of the 33rd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.245-256, January 11-13, 2006, Charleston, South Carolina, USA
• 12: Susan L. Graham , Peter B. Kessler , Marshall K. Mckusick, Gprof: A call graph execution profiler, Proceedings of the 1982 SIGPLAN symposium on Compiler construction, p.120-126, June 23-25, 1982, Boston, Massachusetts, United States
• 13: Klaus Havelund , Grigore Roşu, An Overview of the Runtime Verification Tool Java PathExplorer, Formal Methods in System Design, v.24 n.2, p.189-215, March 2004 [doi>10.1023/B:FORM.0000017721.39909.4b]
• 14: Moonzoo Kim , Mahesh Viswanathan , Sampath Kannan , Insup Lee , Oleg Sokolsky, Java-MaC: A Run-Time Assurance Approach for Java Programs, Formal Methods in System Design, v.24 n.2, p.129-155, March 2004 [doi>10.1023/B:FORM.0000017719.43755.7c]
• 15: Alex Kinneer , Matthew B. Dwyer , Gregg Rothermel, Sofya: Supporting Rapid Development of Dynamic Program Analyses for Java, Companion to the proceedings of the 29th International Conference on Software Engineering, p.51-52, May 20-26, 2007 [doi>10.1109/ICSECOMPANION.2007.68]
• 16: B. Liblit, A. Aiken, and A. Zheng. Distributed program sampling. In Conf. on Prog. Lang. Design and Impl., pages 141--154, 2003.
• 17: S. P. Midkiff , J. E. Moreira , M. Snir, Optimizing array reference checking in Java programs, IBM Systems Journal, v.37 n.3, p.409-453, 1998
• 18: R. Sekar , V.N. Venkatakrishnan , Samik Basu , Sandeep Bhatkar , Daniel C. DuVarney, Model-carrying code: a practical approach for safe execution of untrusted applications, Proceedings of the nineteenth ACM symposium on Operating systems principles, October 19-22, 2003, Bolton Landing, NY, USA
• 19: http://sofya.unl.edu.
• 20: 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
• 21: R. Vallée-Rai. SOOT: A Java bytecode optimization framework. Master's thesis, School of Computer Science, McGill University, Montreal, Canada., Oct 2000.

INDEX TERMS

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

Additional Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.4 Software/Program Verification
          Subjects: Assertion checkers
      D.2.5 Testing and Debugging
          Subjects: Monitors; Tracing

General Terms:
Reliability, Verification

Keywords:
optimizing run-time monitors, static error detection