# Relating Alternating Relations for Conformance and Refinement

@article{Janssen2019RelatingAR, title={Relating Alternating Relations for Conformance and Refinement}, author={Ramon Janssen and Frits W. Vaandrager and Jan Tretmans}, journal={arXiv: Formal Languages and Automata Theory}, year={2019} }

Various relations have been defined to express refinement and conformance for state-transition systems with inputs and outputs, such as ioco and uioco in the area of model-based testing, and alternating simulation and alternating-trace containment originating from game theory and formal verification. Several papers have compared these independently developed relations, but these comparisons make assumptions (e.g., input-enabledness), pose restrictions (e.g., determinism - then they all coincide… Expand

#### Figures and Topics from this paper

#### References

SHOWING 1-10 OF 21 REFERENCES

Interface automata

- Computer Science
- ESEC/FSE-9
- 2001

This work presents a light-weight formalism that captures the temporal aspects of software component interfaces through an automata-based language that supports automatic compatability checks between interface models, and thus constitutes a type system for component interaction. Expand

Alternating Refinement Relations

- Computer Science
- CONCUR
- 1998

This paper generalizes the definitions of the simulation and trace containment preorders from labeled transition systems to alternating transition systems, and shows that, like ordinary simulation, alternating simulation can be checked in polynomial time using a fixpoint computation algorithm. Expand

Test Generation with Inputs, Outputs and Repetitive Quiescence

- Computer Science
- Softw. Concepts Tools
- 1996

This paper studies testing based on labelled transition systems, using the assumption that implementations communicate with their environment via inputs and outputs, and a test generation algorithm is given which is proved to produce a sound and exhaustive test suite from a specification. Expand

Matching implementations to specifications: the corner cases of ioco

- Computer Science
- SAC
- 2019

This paper shows that given a specification, one can construct in a standard way a canonical conforming implementation that is very 'close' to the specification; and a refinement preorder on specification models can be defined such that a refined model allows less ioco-conforming implementations. Expand

Model Based Testing with Labelled Transition Systems

- Computer Science
- Formal Methods and Testing
- 2008

This tutorial chapter describes a model based testing theory where models are expressed as labelled transition systems, and compliance is defined with the 'ioco' implementation relation. Expand

An algebraic theory of interface automata

- Computer Science
- Theor. Comput. Sci.
- 2014

A trace-based linear-time refinement is provided, which is the weakest preorder preserving substitutivity of components, and is weaker than the classical alternating simulation defined on interface automata. Expand

Towards quality of model-based testing in the ioco framework

- Computer Science
- JAMAICA 2013
- 2013

A new test suite is defined that aims at transforming the model to which a system under test must conform, in order to reduce the set of test cases, and a canonical representation is given for the newly defined test suite. Expand

Alternating simulation and IOCO

- Computer Science
- International Journal on Software Tools for Technology Transfer
- 2011

It is shown that non-i/o-refinement reduces to a reachability problem and a translation from bounded non-o- Refinement or boundednon-ioco to checking first-order assertions is provided. Expand

Learning I/O Automata

- Computer Science
- CONCUR
- 2010

It is shown that, by exploiting links between three widely used modeling frameworks for reactive systems, any tool for active learning of Mealy machines can be used for learning I/O automata that are deterministic and output determined. Expand

Model-Based Testing of Environmental Conformance of Components

- Computer Science
- FMCO
- 2006

This paper presents an approach for model-based testing of components where only available models are used, and includes an implementation relation, called eco, which formally defines when a component is correct with respect to the components it uses, and a sound and exhaustive test generation algorithm for eco. Expand