期刊
AUTOMATED SOFTWARE ENGINEERING
卷 18, 期 3-4, 页码 263-292出版社
SPRINGER
DOI: 10.1007/s10515-011-0084-1
关键词
Automatic defect detection; Mining specifications; Temporal logic; Computation Tree Logic; Program analysis
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.
作者
我是这篇论文的作者
点击您的名字以认领此论文并将其添加到您的个人资料中。
推荐
暂无数据