Prof. Clemens Dubslaff (Eindhoven): A Variant-Rich View on Quantitative Verification
Wednesday, 28 January, 4 pm, KIT, Computer Science Building (50.34), Room -102
Abstract: Cyber-physical systems underpin critical infrastructures, rendering their correctness and reliability essential. Formal verification methods such as model checking have shown effective, but scalability remains a major challenge due to growing system sizes, hybrid dynamics, and extensive configurability in variant-rich systems. In this talk, Prof. Dubslaff will present different views on quantitative verification for variant-rich systems using probabilistic model checking. The foundation of this work is the tool ProFeat, which implements a feature-oriented approach to modeling and verification. Here, features represent optional or incremental units of functionality, as commonly seen in software product line engineering. Prof. Dubslaff will illustrate an exhaustive reliability analysis across 10^10 variants of an aircraft velocity controller and show how verification results can be interpreted through causal reasoning. He will close with a brief discussion on extensions, namely role-based and ontology-mediated verification. The former allows features to assume different roles depending on context, while the latter connects features with knowledge bases and deals with inconsistencies between system model and domain knowledge.
Bio: Clemens Dubslaff is an Assistant Professor in the Formal System Analysis cluster at Eindhoven University of Technology, The Netherlands. He earned his Ph.D. from Dresden University of Technology, Germany, with a dissertation on the quantitative analysis of configurable and reconfigurable systems. His research focuses on the theory and application of formal methods in software engineering and artificial intelligence.