choice and chance - model-based testing of stochastic behaviour
Marcus Gerhold is a PhD student in the research group Formal Methods and Tools. His supervisors are prof.dr. M.I.A. Stoelinga and prof.dr. J.C. van der Pol from the Faculty of Electrical Engineering, Mathematics and Computer Science.
Probability plays an important role in many computer applications. A vast number of algorithms, protocols and computation methods uses randomisation to achieve their goals. A crucial question then becomes whether such probabilistic systems work as intended. To investigate this, such systems are often subjected to a large number of well-designed test cases, that compare the observed behaviour to a requirements specification. These tests are often created manually, and are thus prone to human errors. Another approach is to create these test cases automatically. Model-based testing is an innovative testing technique rooted in formal methods, that aims at automating this labour intense task. By providing faster and more thorough testing methods at lower cost, it has gained rapid popularity in industry and academia alike. Despite all, classic model-based testing methods are insufficient when dealing with inherently stochastic systems.
This thesis introduces a rigorous model-based testing framework, that is capable to automatically test such systems. We provide correctness verdicts for functional properties, discrete probability choices, and hard and soft real-time constraints. First, the model-based testing landscape is laid out, and related work is discussed. From there on out, the framework is constructed in a clear step-by-step manner. We instantiate a model-based testing framework from the literature to illustrate the interplay of its theoretical components like, e.g., a conformance relation, test cases, and test verdicts. This framework is then conservatively extended by introducing discrete probability choices to the specification language. A last step further extends this probabilistic framework by adding hard and soft real time constraints. Classic functional correctness verdicts are thus extended with goodness of fit methods known from statistics. Proofs of the framework's correctness are presented before its capabilities are exemplified by studying smaller scale case studies known from the literature.
The framework reconciles non-deterministic and probabilistic choices in a fully-fledged way via the use of schedulers. Schedulers then become a subject worth studying on their own. This is done in the second part of this thesis: We introduce an equivalence relation based on schedulers for Markov automata, and compare its distinguishing power to notions of trace distributions and bisimulation relations. Lastly, the power of different scheduler classes for stochastic automata is investigated: We compare reachability probabilities of schedulers belonging to such different classes by altering the information available to them. This induces a hierarchy of scheduler classes, which we illustrate alongside simple examples.
