Uncovering Legacy Code

One of the largest and most widespread issues in the IT world is that of legacy software, i.e. code that is no longer understood to the level required to continue its effective and non-erroneous usage. Regaining sufficient knowledge of legacy software systems, and maintaining them is an arduous and costly process. We believe that currently used textual documentation techniques are incapable of properly capturing knowledge on software and insufficient for handling modern day software complexity and are thus the main cause of legacy software. We nominate formal models as the proper replacement of current documentation techniques. Formal models allow us to capture and document software without, far exceeding the expressive capacities of current solutions. Formal models also enable us to automatically reason about the correctness of said software systems. The problem with introducing formal models to capture the vast amount of unmodelled software out there is however two-fold: First, there is simply too much software out there to allow for manually modelling every software component. Second, once a model has been acquired, we must ensure that the model accurately captures the behaviour of the modelled system. This thesis thus consists of two parts: `Extracting understandable models' and `Verifying the correctness of extracted models. 'In the first part of the thesis we introduce the novel SSTraGen tool, which we demonstrate, through a case study, to be capable of automatically extracting formal models from industrial C++ code. We also define the so-called diamond-pattern, which can often be seen in parallel systems, and introduce an algorithm for finding and replacing these patterns patterns towards improving the readability of general models. The second part of this thesis focusses on verifying the accuracy of models with respect to their implementation. Here, the specific contributions are extending the cones-and-foci proof framework towards divergence-preserving branching-bisimulation, speeding up model-based testing using greedy on-the-fly test case selection, and relating the stable failure refinement relation and ioco relation used within model based testing.