Static Specification Mining Using Automata-Based Abstractions* - Mining Software Specifications: Methodologies and Applications - page 182

automata and use inspection to check if those paths represent correct usage
patterns of the API. If a path turns out to be spurious, we refine the abstrac-
tion to eliminate that path.

6.6.1 Static Inspection
Static inspection can be performed from the client side and the component
side.

6.6.1.1 Static Client Inspection

Static client inspection statically checks whether a given scenario is present
in the code base. Checking for the absence of a scenario is also known as type-
state verification (e.g., [11]). Since checking for a specific scenario only requires
recording the current state of the typestate property, and not a more elaborate
abstraction of the history, it is generally cheaper than mining. Therefore, the
checking procedure can use more precise (and thus costly) heap abstractions
and be used to prune spurious scenarios that are observed as absent from the
code base.

6.6.1.2 Static Component Inspection

Static component inspection statically checks whether a given scenario
might produce an error when executed over the component.
The extreme case of static component inspection is that of [1] and [24],
which exhaustively (and conservatively) explore all client scenarios and the
resulting component behaviors.

6.6.2 Dynamic Inspection
While static inspection is limited, as it still requires some heap abstraction,
dynamic inspection has the advantage that it can also identify imprecision that
results from the heap abstraction.
Similarly to static inspection, dynamic inspection also comes in two flavors:
client side and component side.

Dynamic client-side inspection checks whether a given usage-scenario
may exist in a given code base (under-approximation). This can be im-
plemented by instrumenting client-code to record various events. This
approach is applied by dynamic mining tools such as Daikon [10].

Dynamic component side inspection checks whether a given usage-
scenario may execute without failure over the component. This is an
under-approximation, as the component may fail this sequence only on
specific environment conditions (e.g., only fail the sequence on Mon-
days). It can be performed without the code of the component, but