ºÚÁϸ£ÀûÍø

focused on the Cordis SUITE, a software platform that allows engineers to design machine-control applications using visual diagrams. She developed a method to translate these diagrams into a language that a computer can analyze automatically, enabling model checking. Model checking is a technique that verifies whether software behaves correctly in all possible situations. This approach helps detect subtle errors that might be missed during traditional testing and ensures higher reliability for critical systems.

Bringing research closer to real-world applications

Stramaglia’s methods are not only theoretical but are designed to work with real-world machine-control systems. By ensuring that software behaves as intended, her research can help prevent production delays in factories, improve the safety of industrial robots, and reduce downtime in automated processes.

This shows how formal verification techniques, often considered highly technical, can directly benefit engineers and industries that rely on dependable software every day.

Understanding why software fails

Large and complex software models can be very hard to analyse because the number of possible behaviours grows extremely quickly. Stramaglia’s method simplifies complex parts of the software, making verification faster and more practical for real-world applications.

Traditional model checking only gives a yes or no answer: the software either works correctly or it does not. Stramaglia went further by developing a method to provide explanations when systems fail. These explanations help engineers understand unexpected behaviour and identify how to fix it efficiently.