ioco theory for probabilistic automata

Marcus Gerhold
(University of Twente, Enschede, The Netherlands)
Mariëlle Stoelinga
(University of Twente, Enschede, The Netherlands)

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 πoco relation, show that it conservatively extends ioco and define the concepts of test case, execution and evaluation.

In Nikolay Pakulin, Alexander K. Petrenko and Bernd-Holger Schlingloff: Proceedings Tenth Workshop on Model Based Testing (MBT 2015), London, UK, 18th April 2015, Electronic Proceedings in Theoretical Computer Science 180, pp. 23–40.
Published: 10th April 2015.

ArXived at: http://dx.doi.org/10.4204/EPTCS.180.2 bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org