Presenter
Andrada Alexia Serban
BME, Budapest
Authors
Andrada Alexia Serban
Abstract
Programmable logic controllers (PLCs) are often used in safety-critical industrial automation, and thus require rigorous software verification. While formal verification provides strong mathematical guarantees, dynamic testing remains the primary approach in industrial practice, despite the challenges of evaluating cyclically executed PLC code. Mutation testing can effectively assess and improve these test suites, but engineers still find designing tests for surviving mutants and identifying equivalent mutants challenging. In this talk, I will demonstrate how formal model checking, specifically utilizing the PLCverif framework, can be used for both equivalence detection and test case generation for live mutants. Finally, I'll show how this formal methodology integrates into a broader, AI-driven test improvement and generation framework currently in development.
Slides
TBA