Specification, testing and implementation relations for symbolic-probabilistic systems

We consider the specification and testing of systems where probabilistic information is not given by means of fixed values but as intervals of probabilities. We will use an extension of the finite state machines model where choices among transitions labelled by the same input action are probabilistically resolved. We will introduce our notion of test and we will define how tests are applied to implementations under test. We will also present implementation relations to assess the conformance, up to a level of confidence, of an implementation to a specification. In order to define these relations 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.