Abstract:

Implementation relations, formalizing the notion of correctness of implementations with respect to specifications, are presented for labelled transition systems. Starting from the well-known principles of testing equivalence and refusal testing for transition systems, analogous ideas are applied to transition systems in which the actions can be partitioned into inputs and outputs, and where inputs are always enabled. This leads to a simplification of the testing theory. The relations with the theories of Input/Output Automata and Input-Output State Machines is indicated.