Reconstructing the High-Level Structure of Legacy Code via Software Model Checking: An Experience Report

The high-level structure of control software of reactive systems in many embedded applications can be described in terms of (extended) state machines. The extraction of such state machines from the code itself can be a valuable form of documentation, e.g. to allow developers to familiarise with legacy implementations, or to validate that the actual implementation is consistent with the high-level specifications. In this paper, we present a tool for the automatic extraction of high-level state machines from legacy code using software model checking techniques. The tool works by slicing and abstracting the code under analysis guided by user feedback, and reconstructs the target state machine via a sequence of reachability queries. We demonstrate the usefulness of the tool by applying it for understanding the high-level structure of the code of a legacy controller for an advanced domestic heat pump system, and showing how the extracted information uncovered some unexpected behaviours of the software.