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. R. Alur, P. Cerny, P. Madhusudan, and W. Nam. Synthesis of interface specifications for Java classes. SIGPLAN Not., 40(1):98--109, 2005.
2. G. Ammons, R. Bodik, and J. R. Larus. Mining specifications. In POPL '02: Proceedings of the 29th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, pages 4--16, New York, NY, USA, 2002. ACM Press.
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. D. Chase, M. Wegman, and F. Zadeck. Analysis of pointers and structures. In Proc. ACM Conf. on Programming Language Design and Implementation, pages 296--310, New York, NY, 1990. ACM Press.
5. J. E. Cook and A. L. Wolf. Discovering models of software processes from event-based data. ACM Trans. Softw. Eng. Methodol., 7(3):215--249, 1998.
6. P. Cousot and R. Cousot. Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In POPL '77: Proceedings of the 4th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, pages 238--252, New York, NY, USA, 1977. ACM Press.
7. D. Engler, D. Y. Chen, S. Hallem, A. Chou, and B. Chelf. Bugs as deviant behavior: a general approach to inferring errors in systems code. In SOSP '01: Proceedings of the eighteenth ACM symposium on Operating systems principles, pages 57--72, New York, NY, USA, 2001. ACM Press.
8. M. D. Ernst, J. Cockrell, W. G. Griswold, and D. Notkin. Dynamically discovering likely program invariants to support program evolution. IEEE Transactions on Software Engineering, 27(2):99--123, Feb. 2001.
9. S. Fink, E. Yahav, N. Dor, G. Ramalingam, and E. Geay. Effective typestate verification in the presence of aliasing. In ISSTA '06: Proceedings of the 2006 international symposium on Software testing and analysis, pages 133--144, New York, NY, USA, 2006. ACM Press.
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. V. B. Livshits and T. Zimmermann. Dynamine: Finding common error patterns by mining software revision histories. In Proceedings of the 13th ACM SIGSOFT International Symposium on the Foundations of Software Engineering (FSE-13), pages 296--305, Sept. 2005.
14. D. Mandelin, L. Xu, R. Bodik, and D. Kimelman. Jungloid mining: helping to navigate the API jungle. In PLDI '05: Proceedings of the 2005 ACM SIGPLAN conference on Programming language design and implementation, pages 48--61, New York, NY, USA, 2005. ACM Press.
15. M. G. Nanda, C. Grothoff, and S. Chandra. Deriving object typestates in the presence of inter-object references. In OOPSLA '05: Proceedings of the 20th annual ACM SIGPLAN conference on Object oriented programming, systems, languages, and applications, pages 77--96, New York, NY, USA, 2005. ACM Press.
16. M. Pistoia, D. Reller, D. Gupta, M. Nagnur, and A. K. Ramani. Java 2 Network Security. Prentice Hall PTR, Upper Saddle River, NJ, USA, second edition, August 1999.
17. T. Reps, S. Horwitz, and M. Sagiv. Precise interprocedural dataflow analysis via graph reachability. In Proc. ACM Symp. on Principles of Programming Languages, pages 49--61, 1995.
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. J. Whaley, M. C. Martin, and M. S. Lam. Automatic extraction of object-oriented component interfaces. In Proceedings of the International Symposium on Software Testing and Analysis, pages 218--228. ACM Press, July 2002.
22. J. Yang, D. Evans, D. Bhardwaj, T. Bhat, and M. Das. Perracotta: mining temporal API rules from imperfect traces. In ICSE '06: Proceeding of the 28th international conference on Software engineering, pages 282--291, New York, NY, USA, 2006. ACM Press.
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

• General and reference

  • Cross-computing tools and techniques

    • Verification

• Software and its engineering

  • Software creation and management

    • Designing software

      • Requirements analysis

    • Software development process management

    • Software verification and validation

      • Formal software verification

  • Software organization and properties

    • Software functional properties

      • Formal methods

        • Software verification

• Theory of computation

  • Semantics and reasoning

    • Program reasoning

      • Program verification