Ioco Theory for Probabilistic Automata

TL;DR

This paper introduces a probabilistic extension of the ioco testing framework, enabling model-based testing of systems with probabilistic behaviors such as unreliable communication and randomized algorithms.

Contribution

It develops the { extpi}oco relation, extending classical ioco to handle probabilistic automata, and defines test case execution and evaluation in this context.

Findings

{ extpi}oco relation extends ioco conservatively

Defines test case, execution, and evaluation for probabilistic systems

Addresses a gap in model-based testing for probabilistic behaviors

Abstract

Model-based testing (MBT) is a well-known technology, which allows for automatic test case generation, execution and evaluation. To test non-functional properties, a number of test MBT frameworks have been developed to test systems with real-time, continuous behaviour, symbolic data and quantitative system aspects. Notably, a lot of these frameworks are based on Tretmans' classical input/output conformance (ioco) framework. However, a model-based test theory handling probabilistic behaviour does not exist yet. Probability plays a role in many different systems: unreliable communication channels, randomized algorithms and communication protocols, service level agreements pinning down up-time percentages, etc. Therefore, a probabilistic test theory is of great practical importance. We present the ingredients for a probabilistic variant of ioco and define the {\pi}oco relation, show that it conservatively extends ioco and define the concepts of test case, execution and evaluation.