Mining temporal specifications from object usage
- ASE 2009
by
Andrzej Wasylkowski, Andreas Zeller
ASE 2009: Proceedings of the 2009 IEEE/ACM International Conference on Automated Software Engineering, Pages 295-306, IEEE Computer Society, Los Alamitos, CA, November 2009.
Digital Library via DOI: 10.1109/ASE.2009.30
Abstract
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 Computation Tree Logic (CTL) 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 189 violations of operational preconditions, uncovering 9 unique defects and 36 unique code smells---with 44% true positives in the 50 top-ranked violations.
BibTeX Entry
@inproceedings{wasylkowski-ase-2009,
title = "Mining temporal specifications from object usage",
author = "Andrzej Wasylkowski and Andreas Zeller",
year = "2009",
month = nov,
address = "Los Alamitos, CA",
booktitle = "ASE 2009: Proceedings of the 2009 IEEE/ACM International Conference on Automated Software Engineering",
location = "Auckland, New Zealand",
pages = "295--306",
publisher = "IEEE Computer Society",
doi = "10.1109/ASE.2009.30",
}