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

1 while (not at the end of the trace)
2 read the next event from the trace
3 update the property FSMs
4 update the monitor FSM
5 if (the monitor FSM is in an accepting state)
6 Increase the counter of the monitor FSM by one
7 for each property FSM
8 if (the property FSM is in an accepting state)
9 increase the counter of the property FSM by one
10 reset the property FSM to its start state

FIGURE 8.11: The approximate inference algorithm.

Finally, instrumentation tools have some limitations on the data they can
capture. For example, an instrumentor might not be able to record argument
values and return values. So, the execution trace can miss information such as
the identity of a lock. When there are multiple instances of a lock, the identity
serves as a way to differentiate operations on the locks. If a trace does not
have the identity of a lock or other ways to distinguish different locks, all calls
to acquire or release different locks will appear to be the same events and may
violate the Alternating property.

8.2.5.2 Detecting the Dominant Behavior

To deal with the imperfect traces, we adapt the algorithm from Figure 8.6.
The new algorithm decides what fraction of an execution trace satisfies a prop-
erty template instead of just determining satisfaction of a property template.
The new algorithm partitions the original trace into subtraces, decides whether
each subtrace satisfies a pattern, and computes the fraction of the subtraces
that satisfy a pattern.
We define a subtrace using a regular expression. We call this regular ex-
pression the monitor template and its finite state machine the monitor FSM.
We call the finite state machine of a property template (e.g., Alternating ) the
property FSM. We use P propertytemplate to represent the percentage of a trace
that satisfies a property template. For example, P AL indicates the percentage
of the subtraces that satisfy the Alternating template.
One intuitive definition of a subtrace is P + S + . In addition, the lead-
ing S events form a subtrace and so do the trailing P events. For
example, we partition PSPSPSPSPSPSPSPSPSP into 10 subtraces
PS;PS;PS;PS;PS;PS;PS;PS;PS;P. The rst nine subtraces satisfy the
P ! S property, whereas the last one does not. Therefore, 90% of the sub-
traces satisfy P ! S and P Alternating is 0:90.
The new algorithm tracks one monitor FSM and one or more property
FSMs. As with the original algorithm, it scans the execution trace twice.
The two algorithms differ in how they update the states during the second
scan. Figure 8.11 shows the pseudo-code of the new algorithm. When the