A Sound and Complete Framework for Testing Probabilistic Systems
Marcus Gerhold
Universiteit van Twente
A wide variety of Model Based Testing (MBT) frameworks exist, capable of handling different system aspects, such as functional properties, real-time quantitative aspects, and continuous behavior. However, a rigorous, sound and complete MBT framework that handles probabilistic specifications along with non-determinisms is long overdue.
We introduce a mathematically precise framework, based on the well-established ioco-framework fully capable of dealing with probabilistic systems, powerful enough to detect any statistical deviation up to arbitrary precision. Our framework also allows for probabilistic testing, thus enabling a better control to steer the automated test process.
We illustrate the functionality of our framework by following a small example application.
