期刊名称：International Journal of Computer Science & Technology
印刷版ISSN：2229-4333
电子版ISSN：0976-8491
出版年度：2013
卷号：4
期号：1
页码：461-467
语种：English
出版社：Ayushmaan Technologies
摘要：It is important that programmers and program maintainers understand important properties of the programs they modify and ensure that the changes they make do not alter essential properties in unintended ways. Manually documenting those properties, especially temporal ones that constrain the ordering of events, is difficult and rarely done in practice. We propose an automatic approach to inferring a target system’s temporal properties based on analyzing its event traces. The core of our technique is a set of pre-defined property patterns among a few events. These patterns form a partial order in terms of their strictness. Our approach finds the strictest properties satisfied by a set of events based on the traces. Formal specifications can help with program testing, optimization, refactoring, documentation, and, most importantly, debugging and repair. Unfortunately, formal specifications are difficult to write manually and techniques that infer specifications automatically suffer from 90-99% false positive rates. Consequently, neither option is currently practiced for most software development projects. We present a novel technique that automatically infers partial correctness specifications with a very low false positive rate. We claim that existing specification miners yield false positives because they assign equal weight to all aspects of program behaviour. For example, we grant less credence to duplicate code, infrequently-tested code, and code that has been changed often or recently. By using additional information from the software engineering process, we are able to dramatically reduce this rate. We evaluate our technique in two ways: as a pre-processing step for an existing specification miner and as part of a novel specification inference algorithm. Our technique identifies which traces are most indicative of program behaviour, which allows off-the-shelf mining techniques to learn the same number of specifications using 60% of their original input. To the best of our knowledge, this is the first specification miner with such a low false positive rate, and thus a low associated burden of manual inspection.
