skip to main content
10.1145/1453101.1453150acmconferencesArticle/Chapter ViewAbstractPublication PagesfseConference Proceedingsconference-collections
research-article

Javert: fully automatic mining of general temporal properties from dynamic traces

Published: 09 November 2008 Publication History

Abstract

Program specifications are important for many tasks during software design, development, and maintenance. Among these, temporal specifications are particularly useful. They express formal correctness requirements of an application's ordering of specific actions and events during execution, such as the strict alternation of acquisition and release of locks. Despite their importance, temporal specifications are often missing, incomplete, or described only informally. Many techniques have been proposed that mine such specifications from execution traces or program source code. However, existing techniques mine only simple patterns, or they mine a single complex pattern that is restricted to a particular set of manually selected events. There is no practical, automatic technique that can mine general temporal properties from execution traces.
In this paper, we present Javert, the first general specification mining framework that can learn, fully automatically, complex temporal properties from execution traces. The key insight behind Javert is that real, complex specifications can be formed by composing instances of small generic patterns, such as the alternating pattern ((ab)) and the resource usage pattern ((ab c)). In particular, Javert learns simple generic patterns and composes them using sound rules to construct large, complex specifications. We have implemented the algorithm in a practical tool and conducted an extensive empirical evaluation on several open source software projects. Our results are promising; they show that Javert is scalable, general, and precise. It discovered many interesting, nontrivial specifications in real-world code that are beyond the reach of existing automatic techniques.

References

[1]
M. Acharya, T. Xie, J. Pei, and J. Xu. Mining API patterns as partial orders from source code: from usage scenarios to specifications. In ESEC-FSE '07: Proceedings of the the 6th joint meeting of the European software engineering conference and the ACM SIGSOFT symposium on The foundations of software engineering, pages 25--34, New York, NY, USA, 2007. ACM.
[2]
H. Agrawal and J. R. Horgan. Dynamic program slicing. In PLDI '90: Proceedings of the ACM SIGPLAN 1990 conference on Programming language design and implementation, pages 246--256, 1990.
[3]
R. Alur, P. Černý, P. Madhusudan, and W. Nam. Synthesis of interface specifications for Java classes. In POPL '05: Proceedings of the 32nd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, pages 98--109, 2005.
[4]
G. Ammons, R. Bodík, 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, 2002.
[5]
G. Ammons, D. Mandelin, R. Bodík, and J. R. Larus. Debugging temporal specifications with concept analysis. In PLDI '03: Proceedings of the ACM SIGPLAN 2003 conference on Programming language design and implementation, pages 182--195, New York, NY, USA, 2003. ACM.
[6]
T. Ball and S. K. Rajamani. Automatically validating temporal safety properties of interfaces. In SPIN '01: Proceedings of the 8th international SPIN workshop on Model checking of software, pages 103--122, 2001.
[7]
R. E. Bryant. Graph-based algorithms for boolean function manipulation. IEEE Trans. Comput., 35(8):677--691, 1986.
[8]
C. Csallner and Y. Smaragdakis. Dynamically discovering likely interface invariants. In Proceedings of ICSE, pages 861--864, 2006.
[9]
V. Dallmeier, C. Lindig, A. Wasylkowski, and A. Zeller. Mining object behavior with adabu. In WODA '06: Proceedings of the 2006 international workshop on Dynamic systems analysis, pages 17--24, New York, NY, USA, 2006. ACM.
[10]
M. Das, S. Lerner, and M. Seigle. ESP: Path-sensitive program verification in polynomial time. In PLDI '02: Proceedings of the ACM SIGPLAN 2002 Conference on Programming language design and implementation, pages 57--68, 2002.
[11]
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, 2001.
[12]
M. D. Ernst, A. Czeisler, W. G. Griswold, and D. Notkin. Quickly detecting relevant program invariants. In Proceedings of ICSE, pages 449--458, 2000.
[13]
C. Flanagan, K. R. M. Leino, M. Lillibridge, G. Nelson, J. B. Saxe, and R. Stata. Extended static checking for Java. In Proceedings of PLDI, pages 234--245, 2002.
[14]
M. Gabel and Z. Su. Symbolic mining of temporal specifications. In ICSE '08: Proceedings of the 30th International Conference on Software Engineering, New York, NY, USA, 2008. ACM.
[15]
S. Hangal and M. S. Lam. Tracking down software bugs using automatic anomaly detection. In Proceedings of ICSE, pages 291--301, 2002.
[16]
T. A. Henzinger, R. Jhala, and R. Majumdar. Permissive interfaces. In ESEC/FSE-13: Proceedings of the 10th European software engineering conference held jointly with 13th ACM SIGSOFT international symposium on Foundations of software engineering, pages 31--40, New York, NY, USA, 2005. ACM.
[17]
T. Kremenek, P. Twohey, G. Back, A. Ng, and D. Engler. From uncertainty to belief: inferring the specification within. In USENIX'06: Proceedings of the 7th conference on USENIX Symposium on Operating Systems Design and Implementation, pages 12--12, 2006.
[18]
Z. Li and Y. Zhou. PR-Miner: automatically extracting implicit programming rules and detecting violations in large software code. In Proceedings of ESEC/FSE-13, pages 306--315, 2005.
[19]
D. Lo and S.-C. Khoo. Smartic: towards building an accurate, robust and scalable specification miner. In SIGSOFT '06/FSE-14: Proceedings of the 14th ACM SIGSOFT international symposium on Foundations of software engineering, pages 265--275, New York, NY, USA, 2006. ACM.
[20]
D. Lorenzoli, L. Mariani, and M. Pezze. Automatic generation of software behavioral models. In ICSE '08: Proceedings of the 30th International Conference on Software Engineering, New York, NY, USA, 2008. ACM.
[21]
S. Lu, S. Park, C. Hu, X. Ma, W. Jiang, Z. Li, R. A. Popa, and Y. Zhou. Muvi: automatically inferring multi-variable access correlations and detecting related semantic and concurrency bugs. In SOSP '07: Proceedings of twenty-first ACM SIGOPS symposium on Operating systems principles, pages 103--116, New York, NY, USA, 2007. ACM.
[22]
J. W. Nimmer and M. D. Ernst. Automatic generation of program specifications. In ISSTA '02: Proceedings of the 2002 ACM SIGSOFT international symposium on Software testing and analysis, pages 229--239, New York, NY, USA, 2002. ACM.
[23]
L. Pitt and M. K. Warmuth. The minimum consistent DFA problem cannot be approximated within a polynomial. In STOC '89: Proceedings of the twenty-first annual ACM symposium on Theory of computing, pages 421--432, New York, NY, USA, 1989. ACM.
[24]
M. K. Ramanathan, A. Grama, and S. Jagannathan. Path-sensitive inference of function precedence protocols. In Proceedings of ICSE, pages 240--250, 2007.
[25]
M. K. Ramanathan, A. Grama, and S. Jagannathan. Static specification inference using predicate mining. In Proceedings of PLDI, pages 123--134, 2007.
[26]
S. Shoham, E. Yahav, S. Fink, and M. Pistoia. Gallery of mined specifications. http://tinyurl.com/23qct8 or http://docs.google.com/View?docid=ddhtqgv6_10hbczjd.
[27]
S. Shoham, E. Yahav, S. Fink, and M. Pistoia. Static specification mining using automata-based abstractions. In Proceedings of ISSTA, pages 174--184, 2007.
[28]
A. Wasylkowski, A. Zeller, and C. Lindig. Detecting object usage anomalies. In ESEC-FSE '07: Proceedings of the the 6th joint meeting of the European software engineering conference and the ACM SIGSOFT symposium on The foundations of software engineering, pages 35--44, New York, NY, USA, 2007. ACM.
[29]
W. Weimer and G. Necula. Mining temporal specifications for error detection. In Proceedings of TACAS, pages 461--476, 2005.
[30]
J. Whaley, M. C. Martin, and M. S. Lam. Automatic extraction of object-oriented component interfaces. In ISSTA '02: Proceedings of the 2002 ACM SIGSOFT international symposium on Software testing and analysis, pages 218--228, 2002.
[31]
Y. Xie and A. Aiken. Scalable error detection using boolean satisfiability. In POPL '05: Proceedings of the 32nd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, pages 351--363, 2005.
[32]
J. Yang, D. Evans, D. Bhardwaj, T. Bhat, and M. Das. Perracotta: Mining temporal API rules from imperfect traces. In Proceedings of ICSE, pages 282--291, 2006.

Cited By

View all

Recommendations

Comments

Information & Contributors

Information

Published In

cover image ACM Conferences
SIGSOFT '08/FSE-16: Proceedings of the 16th ACM SIGSOFT International Symposium on Foundations of software engineering
November 2008
369 pages
ISBN:9781595939951
DOI:10.1145/1453101
Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Sponsors

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 09 November 2008

Permissions

Request permissions for this article.

Check for updates

Author Tags

  1. dynamic analysis
  2. formal specifications
  3. specification mining

Qualifiers

  • Research-article

Conference

SIGSOFT '08/FSE-16
Sponsor:

Acceptance Rates

Overall Acceptance Rate 17 of 128 submissions, 13%

Contributors

Other Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

  • Downloads (Last 12 months)37
  • Downloads (Last 6 weeks)2
Reflects downloads up to 13 Feb 2025

Other Metrics

Citations

Cited By

View all
  • (2024)Specification Mining Based on the Ordering Points to Identify the Clustering Structure Clustering Algorithm and Model CheckingAlgorithms10.3390/a1701002817:1(28)Online publication date: 10-Jan-2024
  • (2024)VALIOKnowledge-Based Systems10.1016/j.knosys.2024.112086299:COnline publication date: 18-Oct-2024
  • (2024)LTL Learning on GPUsComputer Aided Verification10.1007/978-3-031-65633-0_10(209-231)Online publication date: 24-Jul-2024
  • (2023)LExecutor: Learning-Guided ExecutionProceedings of the 31st ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering10.1145/3611643.3616254(1522-1534)Online publication date: 30-Nov-2023
  • (2023)A Model for Types and Levels of Automation in Visual Analytics: A Survey, a Taxonomy, and ExamplesIEEE Transactions on Visualization and Computer Graphics10.1109/TVCG.2022.316376529:8(3550-3568)Online publication date: 1-Aug-2023
  • (2023)A Framework for the Unsupervised Inference of Relations Between Sensed Object Spatial Distributions and Robot Behaviors2023 IEEE International Conference on Robotics and Automation (ICRA)10.1109/ICRA48891.2023.10161071(901-908)Online publication date: 29-May-2023
  • (2023)How do programmers fix bugs as workarounds? An empirical study on Apache projectsEmpirical Software Engineering10.1007/s10664-023-10318-728:4Online publication date: 28-Jun-2023
  • (2023)An empirical study on API usages from code search engine and local libraryEmpirical Software Engineering10.1007/s10664-023-10304-z28:3Online publication date: 13-Apr-2023
  • (2022)A Human-in-the-loop Approach to Generate Annotation Usage RulesProceedings of the 32nd Annual International Conference on Computer Science and Software Engineering10.5555/3566055.3566066(91-100)Online publication date: 15-Nov-2022
  • (2022)Distributed Business Process Discovery in Cloud ClustersInternational Journal of Distributed Artificial Intelligence10.4018/IJDAI.30121314:1(1-18)Online publication date: 1-Jan-2022
  • Show More Cited By

View Options

Login options

View options

PDF

View or Download as a PDF file.

PDF

eReader

View online with eReader.

eReader

Figures

Tables

Media

Share

Share

Share this Publication link

Share on social media