##
Reverse Engineering and Testing

### Kirill Bogdanov

Test generation from extended finite state machines (EFSM) can be
utilised to demonstrate conformance of an implementation to a
model. In other words, it is possible to state a number of assumptions
such that if testing finds no defects, a specific conformance relation
between a model and an implementation can be proven. In its
essence, testing explores a system under test and the conclusion of
conformance is a generalisation of this exploration. In a similar way,
reverse-engineering based on observed traces of a system is also a
generalisation from observed traces. The two can be seen to complement
each other, where every time one makes an overapproximation in the course of reverse-engineering, testing can be used to validate it.

My recent work in this area involves

- using constraints derived from static analysis or "domain expertise"
to help reverse-engineering

- using SMT solvers to check whether generalisations work; information
obtained from traces can help SMT solvers make conclusions.

- comparison of state machines (in practice, we can compute a "diff" between arbitrary directed graphs)