Refinement and Partiality for Model-Based Testing

Large and complex software systems are part of our everyday lives, and bugs are an unavoidable part of that. Software testing is an effective and widely used technique to detect these bugs. This may be done manually, by having a tester interact directly with the software system to find any incorrect behaviour. A more sophisticated form of testing is model-based testing, in which a model-based testing tool automatically generates and executes tests. It does so based on a specification model, which expresses which behaviour is or is not allowed. The meaning of this specification model can be defined by a conformance relation. Ioco theory is one model-based testing theory based upon the conformance relation ioco.

A problem of ioco theory is that it is hard to use multiple independent models to test a single implementation at the same time. This is unpractical in a setting in which different specification models are created to express different points of view of the same system, or in a setting in which models are even created independently by different testers. In this thesis, we define composition of independent models and we express how model-based testing can be done using this composition, in order to simultaneously use multiple specification models.

To define the semantics of this composition, we introduce input-failure refinement, which is closely related to ioco. We show that input-failure refinement can be used in the place of ioco, and that it has favourable properties for composition compared to ioco. In particular, it is hard to determine whether one specification model forbirds more behaviour than another specification model according to ioco. The main result of this thesis therefore is a complete theory to compose independent specification models via input-failure refinement.