Automatic Inference and Effective Application of Temporal Specifications - Mining Software Specifications: Methodologies and Applications - page 244

correctness of a system. Suppose we want to learn the temporal specification
of a type of lock. If our target program neglects to release this type of lock
during some executions (due to bugs), running this program would produce
an imperfect trace that fails to exhibit the rule for correctly using the lock.
A dynamic inference technique needs to effectively deal with such imperfect
execution traces; otherwise it would risk missing important specifications in
the inference results. For example, the Strauss specification miner requires
human guidance to tune an imperfect trace so that it can discover important
specifications that would otherwise be missing [3]. Daikon requires 100% sat-
isfaction of a pattern [26], which might exclude important specifications if the
execution trace is imperfect. Although we aim to handle imperfect traces, we
assume that our traces are mostly correct { our target program should exhibit
the desirable behavior most of the time.
Our inference technique must be able to select interesting specifications.
An interesting specification is a specification whose violation would produce
bad consequences. For example, we consider specifications about using crit-
ical system resources such as locks and transactions to be interesting. Such
properties are important because violating them can have serious consequences
such as causing system crashes [5,19] and opening security vulnerabilities [10].
Selecting interesting specifications is important because for a large program
thousands of properties may be inferred, only a small fraction of which are
interesting. We present several techniques that can effectively increase the
percentage of interesting properties in the results.
8.1.2 Contributions
We describe dynamic inference techniques for automatically inferring tem-
poral specifications and experimentally evaluate our techniques on real sys-
tems, as well as several different applications of the inferred properties. Our
dynamic inference techniques address three limitations of prior inference work
described in the previous section:
(a) The inference algorithms scale poorly with the size of the program and
the execution traces.
(b) Previous dynamic inference techniques do not work well in situations
where perfect traces are not available.
(c) A significant portion of the inferred properties are uninteresting. For
small programs, it is feasible to manually select the interesting proper-
ties; for large programs, property selection must be mostly automated.
In particular we make the following contributions in the area of scaling
dynamic inference techniques:
(a) We develop a scalable inference algorithm that can analyze large execu-
tion traces (Section 8.2).