Probabilistic Black-Box Reachability Checking

Speaker:
Martin Tappler, TU Graz, Austria

Abstract:
Testing techniques often face difficulties in scenarios with limited knowledge about the system under test. Model-based testing, for instance, requires a given system model to derive test cases. However, models are often outdated, they may miss some features or may not be available at all, which renders testing ineffective. Approaches, like AutoBlackTest and black box checking, overcome such issues by incrementally gaining knowledge about the system under test through mining system models from test observations. The latter technique allows to check temporal properties of black-box systems by combining model checking, testing, and active automata learning.
However, it is restricted to deterministic systems. Inspired by black box checking, this talk presents probabilistic black-box reachability checking. The proposed method enables testing of stochastic black-box systems with respect to reachability properties. By combining probabilistic model-checking, stochastic automata learning, and testing we generate testing strategies which maximise the probability of observing desired system observations. A potential application scenario is the reliable reproduction of errors that occur rarely during normal system operation.

Biography:
Martin received a Bachelor's and a Master's degree in Computer Science from Graz University of Technology in Austria. He is currently a project assistant and final-year Ph.D. student at the Institute of Software Technology at Graz University of Technology. He is a member of the "formal methods" group led by Bernhard K. Aichernig. His research interests include model-based testing, automata learning and learning-based verification.

Host: Prof. Mauro Pezzè