Model-based testing (MBT) is a systematic way of black-box testing of a system under test (SUT) with respect to behaviour specified in a model. A key concept of MBT is an implementation- or conformance relation: the precise definition of what it means for an SUT to conform to its model.

One of the formal theories for MBT uses labelled transition systems (LTS) as models and ‘ioco’ - Input-Output-COnformance, as conformance relation. The relation ioco, however, has some weird and unpleasant properties: it uses different domains for modelling SUTs and specifications, it is neither reflexive nor transitive, there are specification models that do not allow any conforming SUT, and it cannot be used for stepwise refinement of models.

In the presentation we show: (1) ‘quasi-reflexivity’: the construction of a canonical conforming implementation that is very ‘close’ to the specification; (2) ‘quasi-transitivity’: a refinement preorder on specification models such that a refined model allows less ioco-conforming implementations; (3) the ioco-variant ‘uioco’ that is much simpler in the above aspects, more intuitive, and on more aspects decidable; (4) the relation between the MBT relations ioco and uioco, and the relations ‘alternating simulation’ and ‘alternating-trace containment’, that originate from game theory and formal verification on interface automata. Alternating-trace containment and uioco, though being defined independently in different worlds and for different uses, turn out to be very similar, which suggests that this notion indeed expresses a generic and natural observational refinement relation.

R. Janssen, J. Tretmans, Matching Implementations to Specifications: The Corner Cases of ‘ioco’. ACM/SIGAPP Symp. on Applied Computing, pp. 2196-2205, ACM, 2019. http://doi.acm.org/10.1145/3297280.3297496

R. Janssen, F. Vaandrager, J. Tretmans, Relating Alternating Relations for Conformance and Refinement. iFM 2019, LNCS 11918, 2019. To appear.