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)