skip to main content
10.1145/1368088.1368096acmconferencesArticle/Chapter ViewAbstractPublication PagesicseConference Proceedingsconference-collections
research-article

Symbolic mining of temporal specifications

Published: 10 May 2008 Publication History

Abstract

Program specifications are important in many phases of the software development process, but they are often omitted or incomplete. An important class of specifications takes the form of temporal properties that prescribe proper usage of components of a software system. Recent work has focused on the automated inference of temporal specifications from the static or runtime behavior of programs. Many techniques match a specification pattern (represented by a finite state automaton) to all possible combinations of program components and enumerate the possible matches. Such approaches suffer from high space complexity and have not scaled beyond simple, two-letter alternating patterns (e.g. (ab)*). In this paper, we precisely define this form of specification mining and show that its general form is NP-complete.
We observe a great deal of regularity in the representation and tracking of all possible combinations of system components. This motivates us to introduce a symbolic algorithm, based on binary decision diagrams (BDDs), that exploits this regularity. Our results show that this symbolic approach expands the tractability of this problem by orders of magnitude in both time and space. It enables us to mine more complex specifications, such as the common three-letter resource acquisition, usage, and release pattern ((ab+c)*). We have implemented our algorithm in a practical tool and used it to find significant specifications in real systems, including Apache Ant and Hibernate. We then used these specifications to find previously unknown bugs.

References

[1]
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.
[2]
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.
[3]
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.
[4]
M. Berndl, O. Lhoták, F. Qian, L. Hendren, and N. Umanee. Points-to analysis using BDDs. In Proceedings of PLDI, pages 103--114, 2003.
[5]
B. Bollig and I. Wegener. Improving the variable ordering of OBDDs is NP-complete. IEEE Trans. Comput., 45(9):993--1002, 1996.
[6]
R. E. Bryant. Graph-based algorithms for boolean function manipulation. IEEE Trans. Comput., 35(8):677--691, 1986.
[7]
H. Chen and D. Wagner. MOPS: an infrastructure for examining security properties of software. In CCS ?02: Proceedings of the 9th ACM conference on Computer and communications security.
[8]
C. Csallner and Y. Smaragdakis. Dynamically discovering likely interface invariants. In Proceedings of ICSE, pages 861--864, 2006.
[9]
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.
[10]
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.
[11]
M. D. Ernst, A. Czeisler, W. G. Griswold, and D. Notkin. Quickly detecting relevant program invariants. In Proceedings of ICSE, pages 449--458, 2000.
[12]
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.
[13]
S. Hangal and M. S. Lam. Tracking down software bugs using automatic anomaly detection. In Proceedings of ICSE, pages 291--301, 2002.
[14]
D. Hovemeyer and W. Pugh. Finding bugs is easy. In OOPSLA ?04: Companion to the 19th annual ACM SIGPLAN conference on Object-oriented programming systems, languages, and applications, pages 132--136, 2004.
[15]
R. Karp. Reducibility among combinatorial problems. In Complexity of Computer Computations. New York.
[16]
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.
[17]
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.
[18]
M. K. Ramanathan, A. Grama, and S. Jagannathan. Path-sensitive inference of function precedence protocols. In Proceedings of ICSE, pages 240--250, 2007.
[19]
M. K. Ramanathan, A. Grama, and S. Jagannathan. Static specification inference using predicate mining. In Proceedings of PLDI, pages 123--134, 2007.
[20]
S. Shoham, E. Yahav, S. Fink, and M. Pistoia. Static specification mining using automata-based abstractions. In Proceedings of ISSTA, pages 174--184, 2007.
[21]
W. Weimer and G. Necula. Mining temporal specifications for error detection. In Proceedings of TACAS, pages 461--476, 2005.
[22]
J. Whaley and M. S. Lam. Cloning-based context-sensitive pointer alias analysis using binary decision diagrams. In Proceedings of PLDI, pages 131--144, 2004.
[23]
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.
[24]
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.
[25]
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.
[26]
X. Zhang, R. Gupta, and Y. Zhang. Efficient forward computation of dynamic slices using reduced ordered binary decision diagrams. In Proceedings of ICSE, 2004.

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)LTL Learning on GPUsComputer Aided Verification10.1007/978-3-031-65633-0_10(209-231)Online publication date: 24-Jul-2024
  • (2023)Supervised Bayesian specification inference from demonstrationsThe International Journal of Robotics Research10.1177/0278364923120465942:14(1245-1264)Online publication date: 4-Oct-2023
  • Show More Cited By

Recommendations

Comments

Information & Contributors

Information

Published In

cover image ACM Conferences
ICSE '08: Proceedings of the 30th international conference on Software engineering
May 2008
558 pages
ISBN:9781605580791
DOI:10.1145/1368088
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: 10 May 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

ICSE '08
Sponsor:

Acceptance Rates

ICSE '08 Paper Acceptance Rate 56 of 370 submissions, 15%;
Overall Acceptance Rate 276 of 1,856 submissions, 15%

Upcoming Conference

ICSE 2025

Contributors

Other Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

  • Downloads (Last 12 months)28
  • 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)LTL Learning on GPUsComputer Aided Verification10.1007/978-3-031-65633-0_10(209-231)Online publication date: 24-Jul-2024
  • (2023)Supervised Bayesian specification inference from demonstrationsThe International Journal of Robotics Research10.1177/0278364923120465942:14(1245-1264)Online publication date: 4-Oct-2023
  • (2023)Towards Strengthening Formal Specifications with Mutation Model CheckingProceedings of the 31st ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering10.1145/3611643.3613080(2102-2106)Online publication date: 30-Nov-2023
  • (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
  • (2022)Isadora: automated information-flow property generation for hardware security verificationJournal of Cryptographic Engineering10.1007/s13389-022-00306-w13:4(391-407)Online publication date: 11-Nov-2022
  • (2022)Dynamic Specification Mining Based on TransformerTheoretical Aspects of Software Engineering10.1007/978-3-031-10363-6_16(220-237)Online publication date: 2022
  • (2021)IsadoraProceedings of the 5th Workshop on Attacks and Solutions in Hardware Security10.1145/3474376.3487286(5-15)Online publication date: 19-Nov-2021
  • (2021)Automatic Animal Behavior Analysis: Opportunities for Combining Knowledge Representation with Machine LearningProcedia Computer Science10.1016/j.procs.2021.04.187186(661-668)Online publication date: 2021
  • (2021)General past-time linear temporal logic specification miningCCF Transactions on High Performance Computing10.1007/s42514-021-00079-43:4(393-406)Online publication date: 19-Oct-2021
  • 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