Specifications are important for many activities during software construction and maintenance process such as testing, verification, debugging and repairing. Despite their importance, specifications are often missing, informal or incomplete because they are difficult to write manually. Many techniques have been proposed to automatically mine specifications describing method call sequence from execution traces or source code using frequent pattern mining. Unfortunately, a sizeable number of such interesting specifications discovered by frequent pattern mining may not capture the correct use patterns of method calls. Consequently, when used in software testing or verification, these mined specifications lead to many false positive defects, which in turn consume much effort for manual investigation.
We present a novel framework for automatically discovering legitimate specifications from execution traces using a mutation testing based approach. Such an approach gives a semantics bearing to the legitimacy of the discovered specifications. We introduce the notion of maximal precision and completeness as the desired forms of discovered specifications, and describe in detail suppression techniques that aid efficient discovery. Preliminary evaluation of this approach on several open source software projects shows that specifications discovered through our approach, compared with those discovered through frequent pattern mining, are much more precise and complete. When used in finding bugs, our specifications also locate defects with significantly fewer false positives and more true positives.

Specification mining techniques are used to automatically infer interaction specifications among objects in the format of call sequences; however, many of these specifications can be meaningless or insignificant. As a consequence, when used in program testing of formal verification, the presence of these leads to false positive defects, which in turn demand much effort for manual investigation. We propose a novel process for determining and extracting significant specifications from a set of mined specifications using mutation testing. The resulting specifications can then be used with program verification to detect defects with high accuracy. To our knowledge, this is the first fully automatic approach for extracting significant specifications from mining using program testing. We evaluate our approach through mining significant specifications for the Java API and use them to find real defects in many system.

Model checking is a powerful and promising approach to software verification. However, many modern model checking systems are still not efficient enough to be applied broadly in practice. One of the problems pertaining to model checking is the ability to verify efficiently rich specifications for large scale software, formally called the specification specific problem. In this project, we study the specification specific problem for Java Pathfinder, a modern model checker for Java programs. We implement Jpf-Ltl, a runtime model checker for linear temporal logic specifications and Java programs, which is built on top of the Java Pathfinder model checker. Jpf-Ltl supports verification of rich configuration events, such as method invocations with object instance aware or local and global program variables. We evaluate Jpf-Ltl on JavaCup and jDepend projects. Result shows that our tool is scalable to complex LTL specifications and Java programs.

You can get a hard copy of the book here. Unfortunately, it's only available in Vietnamese! But don't worry, I do translate some of the articles in English and make them available at this website.