Testing of symbolic-probabilistic systems

In this paper we consider the testing, of systems where probabilistic information is not given by means of fixed values but as sets of probabilities. We will use an extension of finite state machine where choices among transitions labeled by the same input are probabilistically resolved. We will introduce our notion of test and we will define how tests are applied to the implementation under test (IUT). We will also present an implementation relation to assess the conformance, up to a level of confidence, of an implementation to a specification. In order to define this relation we will take finite samples of executions of the implementation and compare them with the probabilistic constraints imposed by the specification. Finally, we will give an algorithm for deriving sound and complete test suites with respect to this implementation relation.