Dynamically inferring, refining, and checking API usage protocols

ABSTRACT

Using a set of API methods often requires compliance with a protocol, whose violation can lead to errors in the program. However, most APIs lack explicit and formal definitions of these protocols. We propose a dynamic program analysis for automatically inferring and refining specifications of correct method call sequences. Our experiments with several Java programs show that we can infer meaningful protocols, such as widely respected programming rules. Furthermore, our analysis finds violations of the inferred specifications that point out potential bugs to the programmer.

REFERENCES

• 1: Glenn Ammons, Rastislav Bodik, and James R. Larus. Mining specifications. In POPL, 2002.
• 2: Kevin Bierhoff and Jonathan Aldrich. Modular typestate checking of aliased objects. In OOPSLA, 2007.
• 3: Stephen M. Blackburn et al. The DaCapo benchmarks: Java benchmarking development and analysis. In OOPSLA, 2006.
• 4: Feng Chen and Grigore Rosu. MOP: An efficient and generic runtime verification framework. In OOPSLA, 2007.
• 5: Michael Dean Ernst. Dynamically discovering likely program invariants. PhD thesis, University of Washington, 2000.
• 6: Mark Gabel and Zhendong Su. Javert: Fully automatic mining of general temporal properties from dynamic traces. In FSE, 2008.
• 7: Michael Pradel and Thomas R. Gross. Automatic generation of object usage specifications from large method traces. In ASE, 2009.
• 8: John Whaley, Michael C. Martin, and Monica S. Lam. Automatic extraction of object-oriented component interfaces. In ISSTA, 2002.
• 9: Jinlin Yang, David Evans, Deepali Bhardwaj, Thirumalesh Bhat, and Manuvir Das. Perracotta: Mining temporal API rules from imperfect traces. In ICSE, 2006.

INDEX TERMS

Primary Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.5 Testing and Debugging

General Terms:
Languages, Reliability, Verification

Keywords:
runtime verification, specification mining