Abstractions for Reverse Engineering

Increasingly sophisticated systems are being integrated into our daily lives, raising the need to verify their safety and reliability. Formal methods offer a range of techniques for providing sound guarantees of a system's correctness with respect to its specification. The continuous evolution of technology encourages the replacement of existing systems with more modern, efficient, and sustainable solutions. However, such modernization is often hindered by the lack of formal requirements and documentation in legacy systems, especially those developed long ago with obsolete technologies and intricate low-level optimizations. This thesis focuses on the problem of reverse engineering, which is the process of extracting relevant specifications from existing systems. The extracted information should be sufficiently abstract and general to support the validation of a new system implementing the same functionality. The properties should focus on observable behavior and should not require the two systems to align in their internal implementation details. We propose a novel approach for reverse engineering based on the concept of stability, a user-defined criterion for identifying points of interest in a system. Our approach is suitable for extracting transactional properties from continuously evolving analog systems, enabling the comparison with digital re-implementations. We apply our approach in the context of an industrial project with the Italian Railway Network, which is currently migrating their interlocking systems from a legacy analog implementation to a new software-based one. Our contribution includes defining an SMT-encoding of relay-based circuits in timed transition systems, and a set of SMT-based optimizations. From the circuits, we effectively extract stable properties and test cases, which we then use to validate the new software. Crucially, we identified bugs that caused the software to deviate from the legacy implementation.