Speaker: Andrea Manini
PHD Student in Information Technology
DEIB - BIO1 Room (Bld. 21)
June 6th, 2025 | 2.30 pm
Contact: Prof. Giovanni Quattrocchi
Abstract
On June 6th, 2025 at 2.30 pm a new appointment of DEEPSE Forum Seminars series titled "Random Testing of Verification Tools for Timed Automata with Automated Oracle Generation" will take place at DEIB BIO1 Room (Building 21).A central challenge in formal verification is ensuring the correctness of software artifacts—typically verification tools—to prevent catastrophic consequences in safety-critical domains. As new theoretical models are frequently introduced, formal verification tools may not have been thoroughly tested due to the lack, or even absence, of suitable test suites and benchmarks. To address this practical limitation, we propose an innovative testing framework that combines random testing techniques with automated oracle generation. This framework is currently tailored for formal verification tools operating on different variants of Timed Automata (TA). The framework is based on a modular variant of TA, known as Tiled Timed Automata, used to derive an oracle that predicts the correct outcome of each test case. We demonstrate the practical applicability of our framework, illustrate its adaptability to different TA variants and their associated decidable problems, and outline how it can support the development of novel theoretical models and formal verification tools.