This Article 
 Bibliographic References 
 Add to: 
Static Specification Mining Using Automata-Based Abstractions
Sept.-Oct. 2008 (vol. 34 no. 5)
pp. 651-666
Sharon Shoham, Technion, Haifa
Eran Yahav, IBM Research, Hawthorne
Stephen J. Fink, IBM Research, Hawthorne
Marco Pistoia, IBM Research, Hawthorne
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.

[1] R. Alur, P. Cerny, P. Madhusudan, and W. Nam, “Synthesis of Interface Specifications for Java Classes,” SIGPLAN Notices, vol. 40, no. 1, pp. 98-109, 2005.
[2] G. Ammons, R. Bodik, and J.R. Larus, “Mining Specifications,” Proc. 29th ACM SIGPLAN-SIGACT Symp. Principles of Programming Languages, pp. 4-16, 2002.
[3] L.O. Andersen, “Program Analysis and Specialization for the C Programming Language,” PhD dissertation (DIKU Report 94/19), DIKU, Univ. of Copenhagen, May 1994.
[4] D. Chase, M. Wegman, and F. Zadeck, “Analysis of Pointers and Structures,” Proc. ACM Conf. Programming Language Design and Implementation, pp. 296-310, 1990.
[5] J.E. Cook and A.L. Wolf, “Discovering Models of Software Processes from Event-Based Data,” ACM Trans. Software Eng. Methodology, vol. 7, no. 3, pp. 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 Fix Points,” Proc. Fourth ACM SIGACT-SIGPLAN Symp. Principles of Programming Languages, pp. 238-252, 1977.
[7] V. Dallmeier, C. Lindig, A. Wasylkowski, and A. Zeller, “Mining Object Behavior with ADABU,” Proc. Int'l Workshop Dynamic Systems Analysis, pp. 17-24, 2006.
[8] B. Demsky and M. Rinard, “Role-Based Exploration of Object-Oriented Programs,” Proc. 24th Int'l Conf. Software Eng., pp. 313-324, 2002.
[9] 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,” Proc. 18th ACM Symp. Operating Systems Principles, pp. 57-72, 2001.
[10] M.D. Ernst, J. Cockrell, W.G. Griswold, and D. Notkin, “Dynamically Discovering Likely Program Invariants to Support Program Evolution,” IEEE Trans. Software Eng., vol. 27, no. 2, pp. 99-123, Feb. 2001.
[11] S. Fink, E. Yahav, N. Dor, G. Ramalingam, and E. Geay, “Effective Typestate Verification in the Presence of Aliasing,” Proc. Int'l Symp. Software Testing and Analysis, pp. 133-144, 2006.
[12] Gallery of Mined Specification, http://tinyurl.com23qct8, , 2008.
[13] E.M. Gold, “Language Identification in the Limit,” Information and Control, vol. 10, pp. 447-474, 1967.
[14] S. Hangal and M.S. Lam, “Tracking Down Software Bugs Using Automatic Anomaly Detection,” May 2002.
[15] V. Kuncak, P. Lam, and M. Rinard, “Role Analysis,” Proc. 29th ACM SIGPLAN-SIGACT Symp. Principles of Programming Languages, Jan. 2002.
[16] P. Lam and M. Rinard, “A Type System and Analysis for the Automatic Extraction and Enforcement of Design Information,” Proc. 17th European Conf. Object-Oriented Programming, 2003.
[17] D. Lie, A. Chou, D. Engler, and D.L. Dill, “A Simple Method for Extracting Models for Protocol Code,” Proc. 28th Ann. Int'l Symp. Computer Architecture, pp. 192-203, 2001.
[18] V.B. Livshits and T. Zimmermann, “Dynamine: Finding Common Error Patterns by Mining Software Revision Histories,” Proc. 13th ACM SIGSOFT Int'l Symp. Foundations of Software Eng., pp. 296-305, Sept. 2005.
[19] D. Lo and S.-C. Khoo, “SMArTIC: Towards Building an Accurate, Robust and Scalable Specification Miner,” Proc. 14th ACM SIGSOFT Int'l Symp. Foundations of Software Eng., pp. 265-275, 2006.
[20] D. Lorenzoli, L. Mariani, and M. Pezzè, “Towards Self-Protecting Enterprise Applications,” Proc. 18th IEEE Int'l Symp. Software Reliability Eng., Nov. 2007.
[21] D. Mandelin, L. Xu, R. Bodik, and D. Kimelman, “Jungloid Mining: Helping to Navigate the API Jungle,” Proc. ACM SIGPLAN Conf. Programming Language Design and Implementation, pp. 48-61, 2005.
[22] L. Mariani and M. Pezzè, “Dynamic Detection of COTS Components Incompatibility,” IEEE Software, vol. 24, no. 5, pp.76-85, Sept./Oct. 2007.
[23] M.G. Nanda, C. Grothoff, and S. Chandra, “Deriving Object Typestates in the Presence of Inter-Object References,” Proc. 20th Ann. ACM SIGPLAN Conf. Object Oriented Programming, Systems, Languages, and Applications, pp. 77-96, 2005.
[24] M. Pistoia, D. Reller, D. Gupta, M. Nagnur, and A.K. Ramani, Java 2 Network Security, second ed. Prentice Hall PTR, Aug. 1999.
[25] T. Reps, S. Horwitz, and M. Sagiv, “Precise Interprocedural Dataflow Analysis via Graph Reachability,” Proc. 32nd ACM SIGPLAN-SIGACT Symp. Principles of Programming Languages, pp.49-61, 1995.
[26] A. Salcianu and M. Rinard, “Purity and Side Effect Analysis for Java Programs,” Proc. Sixth Int'l Conf. Verification, Model Checking, and Abstract Interpretation, 2005.
[27] WALA: The T.J. Watson Libraries for Analysis, http:/wala., 2008.
[28] A. Wasylkowski, A. Zeller, and C. Lindig, “Detecting Object Usage Anomalies,” Proc. Sixth Joint Meeting of the European Software Eng. Conf. and the ACM SIGSOFT Symp. Foundations of Software Eng., pp. 35-44, 2007.
[29] W. Weimer and G. Necula, “Mining Temporal Specifications for Error Detection,” Proc. Int'l Conf. Tools and Algorithms for the Construction and Analysis of Systems, 2005.
[30] J. Whaley, M.C. Martin, and M.S. Lam, “Automatic Extraction of Object-Oriented Component Interfaces,” Proc. Int'l Symp. Software Testing and Analysis, pp. 218-228, July 2002.
[31] J. Yang, D. Evans, D. Bhardwaj, T. Bhat, and M. Das, “Perracotta: Mining Temporal API Rules from Imperfect Traces,” Proc. 28th Int'l Conf. Software Eng., pp. 282-291, 2006.
[32] G. Yorsh, E. Yahav, and S. Chandra, “Symbolic Summarization with Applications to Typestate Verification,” technical report, Tel Aviv Univ.,, 2007.

Index Terms:
Specification, Formal methods, Validation, Software/Program Verification, Specifying and Verifying and Reasoning about Programs
Sharon Shoham, Eran Yahav, Stephen J. Fink, Marco Pistoia, "Static Specification Mining Using Automata-Based Abstractions," IEEE Transactions on Software Engineering, vol. 34, no. 5, pp. 651-666, Sept.-Oct. 2008, doi:10.1109/TSE.2008.63
Usage of this product signifies your acceptance of the Terms of Use.