by Marcus Gerholdt
Everybody likes testing, and everybody likes statistics… So let’s combine the two… In many large systems probability plays an important role, think of randomization in games, encryption, network traffic, etc. Probabilistic model checking tools exist, but are not often used in practice. They combine conformance testing, hypothesis testing and timed testing. The idea is again black box: the specification is a formal method, we give the black box some input based on the formal model, and test whether we get the expected output distribution. In this case, they extended the ioco relation to capture probabilities as well: pioco. It sounds simple to generate test cases, but how about the statistics? Think of sampling to compare distributions using Chi-square testing, hypothesis testing via hypothesis scheduling.
Another important aspect is time: you want the system to react in time. Under the hood they use markov automata (i.e., exponential distributions). For general distributions, they can do the sampling procedure again, and then do the Kolmogorov-Smirnov test for goodness-of-fit. This test builds a step function to see whether this step function approaches the real function. As an example, they looked into the Bluetooth protocol.