LtRules: an automated software library usage rule extraction tool

ABSTRACT

The need to manually specify temporal properties of software systems is a major barrier to wider adoption of software model checking, because the specification of software temporal properties is a difficult, time-consuming, and error-prone process. To address this problem, we propose to automatically extract software library usage rules, which are one type of temporal specifications. Our approach uses a model checker to check a set of software library usage rule candidates against known good programs using that library, and identifies valid rules based on model checking results. These valid rules can help programmers learn about common software library usage. They can also be used to check new programs using the same library. We have implemented our approach in an Eclipse plug-in named LtRules, which can extract software library usage rules from C programs using BLAST as the underlying model checker.

REFERENCES

• 1: OpenSSL: http://www.openssl.org/.
• 2: 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
• 3: 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
• 4: T. Ball, V. Levin, and F. Xie. Automatic creation of environment models viatraining. In TACAS'04: Proceedings of the 10th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, pages 93--107, 2004.
• 5: Thomas Ball , Sriram K. Rajamani, The SLAM project: debugging system software via static analysis, Proceedings of the 29th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.1-3, January 16-18, 2002, Portland, Oregon
• 6: Edmund M. Clarke, Jr. , Orna Grumberg , Doron A. Peled, Model checking, MIT Press, Cambridge, MA, 2000
• 7: 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
• 8: Michael D. Ernst , Jake Cockrell , William G. Griswold , David Notkin, Dynamically Discovering Likely Program Invariants to Support Program Evolution, IEEE Transactions on Software Engineering, v.27 n.2, p.99-123, February 2001 [doi>10.1109/32.908957]
• 9: T. A. Henzinger, R. Jhala, R. Majumdar, and G. Sutre. Software verification with BLAST. In SPIN'03: Proceedings of the 10th International SPIN Workshop on Model Checking of Software, pages 235--239, 2003.
• 10: W. Weimer and G. Necula. Mining temporal specifications for error detection. In TACAS'05: Proceedings of the 11th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, 2005.
• 11: 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
• 12: Jinlin Yang , David Evans, Automatically Inferring Temporal Properties for Program Evolution, Proceedings of the 15th International Symposium on Software Reliability Engineering (ISSRE'04), p.340-351, November 02-05, 2004 [doi>10.1109/ISSRE.2004.11]

INDEX TERMS

Primary Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.4 Software/Program Verification

General Terms:
Verification

Keywords:
model checking, software library usage rule