ºÚÁϸ£ÀûÍø

Legacy software can be difficult to understand because it often evolved over many years, is maintained by engineers who were not involved in its original creation, and sometimes lacks complete documentation. Yet these systems must continue running reliably, as they often support critical operations in healthcare, finance, and manufacturing.

PhD researcher Flip van Spaendonck addressed this challenge by using formal models, precise mathematical descriptions of software behavior. These models are like a blueprint of a software’s behavior, written in mathematical language so it can be analyzed and verified with certainty. This allows engineers to systematically document, analyze, and verify legacy systems, revealing their inner workings and ensuring they behave correctly. Van Spaendonck defended his thesis on Wednesday, November 12.

Extracting formal models from existing code

A major part of work is the , which automatically transforms existing C++ code into formal process models. This allows engineers to understand the behavior of legacy systems without manually dissecting thousands of lines of code. SSTraGen has been applied to real-world software at , proving its effectiveness in industrial settings.

Understanding parallel software patterns

Van Spaendonck also studied the a recurring structure in highly parallel systems. He formalized this pattern mathematically and developed an algorithm to detect all diamonds in any model. This helps engineers analyze complex, concurrent software and ensures the formal models accurately reflect how the system behave.

Verifying software correctness

To check that a model truly matches the original software, Van Spaendonck extended the , a method that compares system behavior step-by-step, making it easier to demonstrate that the model and the actual implementation behave the same. This approach was applied to the , showing that the implementation behaves exactly as specified.

Faster and more reliable testing

He also introduced a for model-based testing, significantly speeding up automated testing compared with standard methods. He also developed the concept of stable-failure traces, which helps identify inconsistencies between software and its model. Both contributions were validated through industrial case studies.