ioco

ioco, short for input-output conformance, is a formal conformance relation used in model-based testing of reactive systems. It compares a specification S and an implementation I modeled as labeled transition systems with distinct input and output actions (and possibly a quiescence action). Introduced by Jan Tretmans in the late 1990s, ioco provides a criterion to decide whether I behaves according to S under any sequence of environment inputs and observed outputs.

The core idea is trace-based: for every finite trace σ that can occur in the specification, the set of outputs that the implementation can produce after σ must be a subset of the outputs allowed by the specification after σ. In short, after any history, I must not emit an output that S would not emit. Quiescence (no output) is treated as an observable output, so the spec must also permit it after histories.

ioco underpins automated test generation: from a finite-state specification, a test suite can be derived that, when run against an implementation, detects non-conformance by observing unexpected outputs or prohibited behavior. It is applicable to hardware, software, and embedded systems and accommodates nondeterministic specifications.

Tools such as JTorX implement ioco-based conformance testing, and the approach has influenced model-based testing practice and research, including variants that incorporate quiescence and richer modeling formalisms.