Mining temporal specifications from object usage
by Andrzej Wasylkowski, Andreas Zeller

Automated Software Engineering, Pages 263-292, Volume 18, Number 3-4, Springer US, December 2011.

Digital Library via DOI: 10.1007/s10515-011-0084-1


A caller must satisfy the callee's precondition?that is, reach a state in which the callee may be called. Preconditions describe the state that needs to be reached, but not how to reach it. We combine static analysis with model checking to mine Fair Computation Tree Logic (CTL F ) formulas that describe the operations a parameter goes through: "In parseProperties(String xml), the parameter xml normally stems from getProperties()." Such operational preconditions can be learned from program code, and the code can be checked for their violations. Applied to AspectJ, our Tikanga prototype found 169 violations of operational preconditions, uncovering 7 unique defects and 27 unique code smells?with 52% true positives in the 25% top-ranked violations.

BibTeX Entry

    title = "Mining temporal specifications from object usage",
    author = "Andrzej Wasylkowski and Andreas Zeller",
    year = "2011",
    month = dec,
    journal = "Automated Software Engineering",
    number = "3-4",
    pages = "263--292",
    publisher = "Springer US",
    volume = "18",
    doi = "10.1007/s10515-011-0084-1",

Show all publications of the Software Engineering Chair.