Adapting Grammar Inference Techniques to Mine State Machines - Mining Software Specifications: Methodologies and Applications - page 79

is not the case, the counter-examples are used to build a new PLTS 0 , and
new candidate state merges are computed (lines 26{27). Otherwise, if there
are no counter-examples, a set of queries is generated. 3 For each query, the
user is given the opportunity to answer it with a new LTL constraint, in which
case the process is restarted with the new LTL query (lines 8{10). If no new
LTL queries are supplied, the algorithm carries on as with QSM, allowing the
developer to state whether a query is valid or not.
As with traces, it is unrealistic to expect the developer to supply a suitable
set of LTL constraints without guidance. The QSM process of asking ques-
tions enables this; the developer can either choose to answer queries as they
would with the conventional QSM algorithm, or queries can be answered more
comprehensively with an LTL constraint that will also prevent other similar
questions from being asked. Preliminary results on small case studies have
produced promising results [34]; depending on the initial set of traces and the
supplied set of LTL constraints the number of questions can be substantially
reduced, whilst maintaining or even slightly improving the accuracy of the
inferred machine.
3.5 Conclusions and Future Work
This chapter has presented a selection of advances on the traditional
reverse-engineering process, many of which have been inspired by advances
in the field of grammar inference. The rigid process described in Figure 3.2
has been gradually augmented. The process can be iterative. It can accept
inputs from a developer in the form of answers to queries, from model-based
testers in the form of passed/failed test cases, and from model-checkers in the
form of counter-examples to constraints.
The result is that state machines can be reverse-engineered with less input
required from the user. The collection of traces can be automated with model-
based testers and counter-examples from model checkers. The use of negative
traces reduces the reliance upon primitive heuristics, and enables the inference
of state machines that are much more accurate.
Nonetheless, there still remains a host of important challenges to be ad-
dressed by future work. Current techniques do not account for the task of
abstracting traces into sequences of symbols. A typical trace will record se-
quences of low-level events (i.e., method calls in an object-oriented system).
A relatively trivial program trace can incorporate hundreds of different events
and be extremely large. Current approaches assume that there is some \ab-
straction function" that automatically lifts a low-level trace to a sequence
3 The generateQueries function here is slightly different from QSM; it ensures that none
of the queries contradict the given set of LTL constraints.