Symbolic mining of temporal specifications

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: Rajeev Alur , Pavol Černý , P. Madhusudan , Wonhong Nam, Synthesis of interface specifications for Java classes, Proceedings of the 32nd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.98-109, January 12-14, 2005, Long Beach, California, USA
• 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: Thomas Ball , Sriram K. Rajamani, Automatically validating temporal safety properties of interfaces, Proceedings of the 8th international SPIN workshop on Model checking of software, p.103-122, May 2001, Toronto, Ontario, Canada
• 4: Marc Berndl , Ondrej Lhoták , Feng Qian , Laurie Hendren , Navindra Umanee, Points-to analysis using BDDs, Proceedings of the ACM SIGPLAN 2003 conference on Programming language design and implementation, June 09-11, 2003, San Diego, California, USA
• 5: Beate Bollig , Ingo Wegener, Improving the Variable Ordering of OBDDs Is NP-Complete, IEEE Transactions on Computers, v.45 n.9, p.993-1002, September 1996 [doi>10.1109/12.537122]
• 6: Randal E. Bryant, Graph-Based Algorithms for Boolean Function Manipulation, IEEE Transactions on Computers, v.35 n.8, p.677-691, August 1986 [doi>10.1109/TC.1986.1676819]
• 7: Hao Chen , David Wagner, MOPS: an infrastructure for examining security properties of software, Proceedings of the 9th ACM conference on Computer and communications security, November 18-22, 2002, Washington, DC, USA [doi>10.1145/586110.586142]
• 8: Christoph Csallner , Yannis Smaragdakis, Dynamically discovering likely interface invariants, Proceedings of the 28th international conference on Software engineering, May 20-28, 2006, Shanghai, China [doi>10.1145/1134285.1134435]
• 9: Manuvir Das , Sorin Lerner , Mark Seigle, ESP: path-sensitive program verification in polynomial time, Proceedings of the ACM SIGPLAN 2002 Conference on Programming language design and implementation, June 17-19, 2002, Berlin, Germany
• 10: 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
• 11: Michael D. Ernst , Adam Czeisler , William G. Griswold , David Notkin, Quickly detecting relevant program invariants, Proceedings of the 22nd international conference on Software engineering, p.449-458, June 04-11, 2000, Limerick, Ireland [doi>10.1145/337180.337240]
• 12: Cormac Flanagan , K. Rustan M. Leino , Mark Lillibridge , Greg Nelson , James B. Saxe , Raymie Stata, Extended static checking for Java, Proceedings of the ACM SIGPLAN 2002 Conference on Programming language design and implementation, June 17-19, 2002, Berlin, Germany
• 13: Sudheendra Hangal , Monica S. Lam, Tracking down software bugs using automatic anomaly detection, Proceedings of the 24th International Conference on Software Engineering, May 19-25, 2002, Orlando, Florida [doi>10.1145/581339.581377]
• 14: David Hovemeyer , William Pugh, Finding bugs is easy, Companion to the 19th annual ACM SIGPLAN conference on Object-oriented programming systems, languages, and applications, October 24-28, 2004, Vancouver, BC, CANADA [doi>10.1145/1028664.1028717]
• 15: R. Karp. Reducibility among combinatorial problems. In Complexity of Computer Computations. New York.
• 16: Ted Kremenek , Paul Twohey , Godmar Back , Andrew Ng , Dawson Engler, From uncertainty to belief: inferring the specification within, Proceedings of the 7th USENIX Symposium on Operating Systems Design and Implementation, p.12-12, November 06-08, 2006, Seattle, WA
• 17: Zhenmin Li , Yuanyuan Zhou, PR-Miner: automatically extracting implicit programming rules and detecting violations in large software code, 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
• 18: Murali Krishna Ramanathan , Ananth Grama , Suresh Jagannathan, Path-Sensitive Inference of Function Precedence Protocols, Proceedings of the 29th international conference on Software Engineering, p.240-250, May 20-26, 2007 [doi>10.1109/ICSE.2007.63]
• 19: Murali Krishna Ramanathan , Ananth Grama , Suresh Jagannathan, Static specification inference using predicate mining, Proceedings of the 2007 ACM SIGPLAN conference on Programming language design and implementation, June 10-13, 2007, San Diego, California, USA
• 20: Sharon Shoham , Eran Yahav , Stephen Fink , Marco Pistoia, Static specification mining using automata-based abstractions, Proceedings of the 2007 international symposium on Software testing and analysis, July 09-12, 2007, London, United Kingdom [doi>10.1145/1273463.1273487]
• 21: W. Weimer and G. Necula. Mining temporal specifications for error detection. In Proceedings of TACAS, pages 461--476, 2005.
• 22: John Whaley , Monica S. Lam, Cloning-based context-sensitive pointer alias analysis using binary decision diagrams, Proceedings of the ACM SIGPLAN 2004 conference on Programming language design and implementation, June 09-11, 2004, Washington DC, USA
• 23: 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
• 24: Yichen Xie , Alex Aiken, Scalable error detection using boolean satisfiability, Proceedings of the 32nd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.351-363, January 12-14, 2005, Long Beach, California, USA
• 25: Jinlin Yang , David Evans , Deepali Bhardwaj , Thirumalesh Bhat , Manuvir Das, Perracotta: mining temporal API rules from imperfect traces, Proceedings of the 28th international conference on Software engineering, May 20-28, 2006, Shanghai, China [doi>10.1145/1134285.1134325]
• 26: Xiangyu Zhang , Rajiv Gupta , Youtao Zhang, Efficient Forward Computation of Dynamic Slices Using Reduced Ordered Binary Decision Diagrams, Proceedings of the 26th International Conference on Software Engineering, p.502-511, May 23-28, 2004

INDEX TERMS

Primary Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.7 Distribution, Maintenance, and Enhancement
          Subjects: Restructuring, reverse engineering, and reengineering

Additional Classification:
  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.1 Specifying and Verifying and Reasoning about Programs

General Terms:
Algorithms, Languages, Verification

Keywords:
dynamic analysis, formal specifications, specification mining