Perracotta: mining temporal API rules from imperfect traces

ABSTRACT

Dynamic inference techniques have been demonstrated to provide useful support for various software engineering tasks including bug finding, test suite evaluation and improvement, and specification generation. To date, however, dynamic inference has only been used effectively on small programs under controlled conditions. In this paper, we identify reasons why scaling dynamic inference techniques has proven difficult, and introduce solutions that enable a dynamic inference technique to scale to large programs and work effectively with the imperfect traces typically available in industrial scenarios. We describe our approximate inference algorithm, present and evaluate heuristics for winnowing the large number of inferred properties to a manageable set of interesting properties, and report on experiments using inferred properties. We evaluate our techniques on JBoss and the Windows kernel. Our tool is able to infer many of the properties checked by the Static Driver Verifier and leads us to discover a previously unknown bug in Windows.

REFERENCES

• 1: Joint CAV/ISSTA Special Event on Specification, Verification, and Testing of Concurrent Software. Jul. 2004.
• 2: T. Andrews, S. Qadeer, J. Rehof, S. K. Rajamani, and Y. Xie. Zing: exploiting program structure for model checking concurrent software. International Conference on Concurrency Theory, Aug./Sep. 2004.
• 3: Rajeev Alur , Pavol Černý , P. Madhusudan , Wonhong Nam, Synthesis of interface specifications for Java classes, Proceedings of the 32nd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.98-109, January 12-14, 2005, Long Beach, California, USA
• 4: Glenn Ammons , Rastislav Bodík , James R. Larus, Mining specifications, Proceedings of the 29th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.4-16, January 16-18, 2002, Portland, Oregon
• 5: Thomas Ball , Sriram K. Rajamani, Automatically validating temporal safety properties of interfaces, Proceedings of the 8th international SPIN workshop on Model checking of software, p.103-122, May 2001, Toronto, Ontario, Canada
• 6: T. M. Bull , E. J. Younger , K. H. Bennett , Z. Luo, Bylands: reverse engineering safety-critical systems, Proceedings of the International Conference on Software Maintenance, p.358, October 17-20, 1995
• 7: J. Bowen, P. Breuer, and K. Lano. Formal specifications in software maintenance: from code to Z++ and back again. Information and Software Technology. Nov./Dec. 1993.
• 8: P. T. Breuer and K. Lano. Creating specifications from code: reverse-engineering techniques. Journal of Software Maintenance: Research and Practice. Vol 3. 1991.
• 9: Sagar Chaki , Edmund Clarke , Alex Groce , Somesh Jha , Helmut Veith, Modular verification of software components in C, Proceedings of the 25th International Conference on Software Engineering, May 03-10, 2003, Portland, Oregon
• 10: Hao Chen , David Wagner, MOPS: an infrastructure for examining security properties of software, Proceedings of the 9th ACM conference on Computer and communications security, November 18-22, 2002, Washington, DC, USA [doi>10.1145/586110.586142]
• 11: Jonathan E. Cook , Zhidian Du , Chongbing Liu , Alexander L. Wolf, Discovering models of behavior for concurrent workflows, Computers in Industry, v.53 n.3, p.297-319, April 2004 [doi>10.1016/j.compind.2003.10.005]
• 12: J. C. Corbett, M. B. Dwyer, J. Hatcliff, and Robby. Expressing checkable properties of dynamic systems: the Bandera specification language. International Journal on Software Tools for Technology Transfer 4(1): 34--56. 2002.
• 13: Manuvir Das , Sorin Lerner , Mark Seigle, ESP: path-sensitive program verification in polynomial time, Proceedings of the ACM SIGPLAN 2002 Conference on Programming language design and implementation, June 17-19, 2002, Berlin, Germany
• 14: Cormac Flanagan , K. Rustan M. Leino , Mark Lillibridge , Greg Nelson , James B. Saxe , Raymie Stata, Extended static checking for Java, Proceedings of the ACM SIGPLAN 2002 Conference on Programming language design and implementation, June 17-19, 2002, Berlin, Germany
• 15: 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]
• 16: Dawson Engler , David Yu Chen , Seth Hallem , Andy Chou , Benjamin Chelf, Bugs as deviant behavior: a general approach to inferring errors in systems code, Proceedings of the eighteenth ACM symposium on Operating systems principles, October 21-24, 2001, Banff, Alberta, Canada
• 17: Michael D. Ernst , Jake Cockrell , William G. Griswold , David Notkin, Dynamically Discovering Likely Program Invariants to Support Program Evolution, IEEE Transactions on Software Engineering, v.27 n.2, p.99-123, February 2001 [doi>10.1109/32.908957]
• 18: David Evans, Static detection of dynamic memory errors, Proceedings of the ACM SIGPLAN 1996 conference on Programming language design and implementation, p.44-53, May 21-24, 1996, Philadelphia, Pennsylvania, United States
• 19: Cormac Flanagan , Rajeev Joshi , K. Rustan M. Leino, Annotation inference for modular checkers, Information Processing Letters, v.77 n.2-4, p.97-108, Feb. 1, 2001 [doi>10.1016/S0020-0190(00)00196-4]
• 20: 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]
• 21: E. Gold. Language identification in the limit. Information and Control, 10, 447--474, 1967.
• 22: E. Gold. Complexity of automatic identification from given data. Information and Control, 37, 302--320, 1978.
• 23: David Grove , Craig Chambers, A framework for call graph construction algorithms, ACM Transactions on Programming Languages and Systems (TOPLAS), v.23 n.6, p.685-746, November 2001 [doi>10.1145/506315.506316]
• 24: N. Gupta. Generating test data for dynamically discovering likely program invariants. Workshop on Dynamic Analysis, May 2003.
• 25: S. Hagnal and M. S. Lam. Tracking down software bugs using automatic anomaly detection. ICSE, May 2002.
• 26: Michael Harder , Jeff Mellen , Michael D. Ernst, Improving test suites via operational abstraction, Proceedings of the 25th International Conference on Software Engineering, May 03-10, 2003, Portland, Oregon
• 27: 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]
• 28: Gerard J. Holzmann, The logic of bugs, Proceedings of the 10th ACM SIGSOFT symposium on Foundations of software engineering, November 18-22, 2002, Charleston, South Carolina, USA [doi>10.1145/587051.587064]
• 29: Java Transaction API specification. http://java.sun.com/products/jta/
• 30: J2EE. http://java.sun.com/j2ee/index.jsp
• 31: JBoss. http://www.jboss.org
• 32: JRat. http://jrat.sourceforge.net/
• 33: J. R. Larus, T. Ball, M. Das, R. DeLine, M. Fahndrich, J. Pincus, S. K. Rajamani, and R. Venkatapathy. Righting Software. IEEE Software, May/Jun. 2004.
• 34: Ben Liblit , Mayur Naik , Alice X. Zheng , Alex Aiken , Michael I. Jordan, Scalable statistical bug isolation, Proceedings of the 2005 ACM SIGPLAN conference on Programming language design and implementation, June 12-15, 2005, Chicago, IL, USA
• 35: Lee Lin , Michael D. Ernst, Improving the adaptability of multi-mode systems via program steering, Proceedings of the 2004 ACM SIGSOFT international symposium on Software testing and analysis, July 11-14, 2004, Boston, Massachusetts, USA
• 36: Benjamin Livshits , Thomas Zimmermann, DynaMine: finding common error patterns by mining software revision histories, Proceedings of the 10th European software engineering conference held jointly with 13th ACM SIGSOFT international symposium on Foundations of software engineering, September 05-09, 2005, Lisbon, Portugal
• 37: Jeremy W. Nimmer , Michael D. Ernst, Invariant inference for static checking:, Proceedings of the 10th ACM SIGSOFT symposium on Foundations of software engineering, November 18-22, 2002, Charleston, South Carolina, USA [doi>10.1145/587051.587054]
• 38: A. Pnueli. The temporal logic of programs. Annual Symposium on Foundations of Computer Science, Oct./Nov. 1977.
• 39: B. Pytlik, M. Renieris, S. Krishnamurthi, and S. P. Reiss. Automated fault localization using potential invariants. International Symposium on Automated and Analysis-Driven Debugging. Sep. 2003.
• 40: Steven P. Reiss , Manos Renieris, Encoding program executions, Proceedings of the 23rd International Conference on Software Engineering, p.221-230, May 12-19, 2001, Toronto, Ontario, Canada
• 41: Thomas Reps , Susan Horwitz , Mooly Sagiv, Precise interprocedural dataflow analysis via graph reachability, Proceedings of the 22nd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.49-61, January 23-25, 1995, San Francisco, California, United States [doi>10.1145/199448.199462]
• 42: Static Driver Verifier: Finding bugs in device drivers at compile-time. WinHEC, Apr. 2004.
• 43: C. Simonyi. Hungarian notation. MSDN library.
• 44: Rachel L. Smith , George S. Avrunin , Lori A. Clarke , Leon J. Osterweil, PROPEL: an approach supporting property elucidation, Proceedings of the 24th International Conference on Software Engineering, May 19-25, 2002, Orlando, Florida [doi>10.1145/581339.581345]
• 45: A. Edwards, A. Srivastava, and H. Vo. Vulcan: binary transformation in a distributed environment. Research Technical Report, MSR-TR-2001-50, Apr. 2001.
• 46: 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
• 47: Willem Visser , Klaus Havelund , Guillaume Brat , Seungjoon Park , Flavio Lerda, Model Checking Programs, Automated Software Engineering, v.10 n.2, p.203-232, April 2003 [doi>10.1023/A:1022920129859]
• 48: W. Weimer and G. Necula. Mining temporal specifications for error detection. International Conference on Tools and Algorithms for the Construction and Analysis of Systems, Apr. 2005.
• 49: John Whaley , Michael C. Martin , Monica S. Lam, Automatic extraction of object-oriented component interfaces, Proceedings of the 2002 ACM SIGSOFT international symposium on Software testing and analysis, July 22-24, 2002, Roma, Italy
• 50: Tao Xie , David Notkin, Tool-assisted unit-test generation and selection based on operational abstractions, Automated Software Engineering, v.13 n.3, p.345-371, July 2006 [doi>10.1007/s10851-006-8530-6]
• 51: Jinlin Yang , David Evans, Dynamically inferring temporal properties, Proceedings of the ACM-SIGPLAN-SIGSOFT workshop on Program analysis for software tools and engineering, June 07-08, 2004, Washington DC, USA [doi>10.1145/996821.996832]
• 52: Jinlin Yang , David Evans, Automatically Inferring Temporal Properties for Program Evolution, Proceedings of the 15th International Symposium on Software Reliability Engineering (ISSRE'04), p.340-351, November 02-05, 2004 [doi>10.1109/ISSRE.2004.11]

INDEX TERMS

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

General Terms:
Experimentation, Reliability, Verification

Keywords:
dynamic analysis, specification inference, temporal properties