Static specification mining using automata-based abstractions

ABSTRACT

We present a novel approach to client-side mining of temporal API specifications based on static analysis. Specifically, we present an interprocedural analysis over a combined domain that abstracts both aliasing and event sequences for individual objects. The analysis uses a new family of automata-based abstractions to represent unbounded event sequences, designed to disambiguate distinct usage patterns and merge similar usage patterns. Additionally, our approach includes an algorithm that summarizes abstract traces based on automata clusters, and effectively rules out spurious behaviors.

We show experimental results mining specifications from a number of Java clients and APIs. The results indicate that effective static analysis for client-side mining requires fairly precise treatment of aliasing and abstract event sequences. Based on the results, we conclude that static client-side specification mining shows promise as a complement or alternative to dynamic approaches.

REFERENCES

• 1: Rajeev Alur , Pavol Černý , P. Madhusudan , Wonhong Nam, Synthesis of interface specifications for Java classes, ACM SIGPLAN Notices, v.40 n.1, p.98-109, January 2005
• 2: 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
• 3: L. O. Andersen. Program Analysis and Specialization for the C Programming Language. PhD thesis, DIKU, Univ. of Copenhagen, May 1994. (DIKU report 94/19).
• 4: David R. Chase , Mark Wegman , F. Kenneth Zadeck, Analysis of pointers and structures, Proceedings of the ACM SIGPLAN 1990 conference on Programming language design and implementation, p.296-310, June 1990, White Plains, New York, United States
• 5: Jonathan E. Cook , Alexander L. Wolf, Discovering models of software processes from event-based data, ACM Transactions on Software Engineering and Methodology (TOSEM), v.7 n.3, p.215-249, July 1998 [doi>10.1145/287000.287001]
• 6: Patrick Cousot , Radhia Cousot, Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints, Proceedings of the 4th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.238-252, January 17-19, 1977, Los Angeles, California [doi>10.1145/512950.512973]
• 7: 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
• 8: 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]
• 9: 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]
• 10: Gallery of mined specification. http://tinyurl.com/23qct8 or http://docs.google.com/View?docid=ddhtqgv6 10hbczjd.
• 11: E. M. Gold. Language identification in the limit. Information and Control, 10:447--474, 1967.
• 12: S. Hangal and M. S. Lam. Tracking down software bugs using automatic anomaly detection. May 2002.
• 13: 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
• 14: David Mandelin , Lin Xu , Rastislav Bodík , Doug Kimelman, Jungloid mining: helping to navigate the API jungle, Proceedings of the 2005 ACM SIGPLAN conference on Programming language design and implementation, June 12-15, 2005, Chicago, IL, USA
• 15: Mangala Gowri Nanda , Christian Grothoff , Satish Chandra, Deriving object typestates in the presence of inter-object references, Proceedings of the 20th annual ACM SIGPLAN conference on Object oriented programming, systems, languages, and applications, October 16-20, 2005, San Diego, CA, USA
• 16: Marco Pistoia , Deepak Gupta , Duane F. Reller , Milind Nagnur , Ashok K. Ramani, Java 2 Network Security, Prentice Hall PTR, Upper Saddle River, NJ, 1999
• 17: 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]
• 18: A. Salcianu and M. Rinard. Purity and side effect analysis for Java programs. In VMCAI'05: Proceedings of the 6th International Conference on Verification, Model Checking, and Abstract Interpretation, 2005.
• 19: WALA: The T. J. Watson Libraries for Analysis. http://wala.sourceforge.net.
• 20: W. Weimer and G. Necula. Mining temporal specifications for error detection. In TACAS, 2005.
• 21: 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
• 22: Jinlin Yang , David Evans , Deepali Bhardwaj , Thirumalesh Bhat , Manuvir Das, Perracotta: mining temporal API rules from imperfect traces, Proceeding of the 28th international conference on Software engineering, May 20-28, 2006, Shanghai, China [doi>10.1145/1134285.1134325]
• 23: G. Yorsh, E. Yahav, and S. Chandra. Symbolic summarization with applications to typestate verification. Technical report, Tel Aviv University, 2007. www.cs.tau.ac.il/~gretay.

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.1 Requirements/Specifications

General Terms:
Algorithms, Verification

Keywords:
abstract interpretation, specification mining, static analysis, typestate