I'm learning about formal languages and Label Transition Systems (LTSs) and how to test systems using Model-Based Testing. Specifically, the paper Model Based Testing with Labelled Transition Systems written by Jan Tretmans. He introduces the concepts ioco (input-output conformance), uioco (underspecified input-output conformance) and tioco (timed input-output conformance). I could follow his description of ioco and how the specification should adhere to the implementation. Or formally defined as:

$i$ ioco $s =_{def} \forall \sigma ∈ Straces(s) $: $output \ (i$ after $\sigma) ⊆ output (s$ after $\sigma) $

Which basically means:

$implementation$ ioco-conforms to $specification$, iff

• if $implementation$ produces output $x$ after trace $\sigma$, then $specification$ can produce $x$ after $\sigma$

• if $implementation$ cannot produce any output after trace $\sigma$, then $specification$ cannot produce any output after $\sigma$

But then I couldn't follow his description of what uioco and tioco mean and couldn't find other sources that explain it differently. Could someone point me out what the latter two concepts are and what the difference between them and ioco is?

P.S. I also couldn't find tags about LTSs nor the concepts of Model Based Testing and input-output conformance, so feel free to edit my tags to something more appropriate.


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.