### Abstract

Original language | Undefined |
---|---|

Article number | 10.1016/S0304-3975(99)00134-6 |

Pages (from-to) | 225-257 |

Number of pages | 33 |

Journal | Theoretical computer science |

Volume | 254 |

Issue number | 1-2 |

DOIs | |

Publication status | Published - 2001 |

### Keywords

- FMT-RT: VERIFICATION OF REAL-TIME SYSTEMS
- METIS-204167
- IR-63254
- FMT-TESTING
- EWI-6371

### Cite this

*Theoretical computer science*,

*254*(1-2), 225-257. [10.1016/S0304-3975(99)00134-6]. https://doi.org/10.1016/S0304-3975(99)00134-6

}

*Theoretical computer science*, vol. 254, no. 1-2, 10.1016/S0304-3975(99)00134-6, pp. 225-257. https://doi.org/10.1016/S0304-3975(99)00134-6

**Testing Timed Automata.** / Springintveld, Jan; Vaandrager, Frits; d' Argenio, P.R.

Research output: Contribution to journal › Article › Academic

TY - JOUR

T1 - Testing Timed Automata

AU - Springintveld, Jan

AU - Vaandrager, Frits

AU - d' Argenio, P.R.

PY - 2001

Y1 - 2001

N2 - We present a generalization of the classical theory of testing for Mealy machines to a setting of dense real-time systems. A model of timed I/O automata is introduced, inspired by the timed automaton model of Alur and Dill, together with a notion of test sequence for this model. Our main contributions is a test suite derivation algorithm for black-box conformance testing of timed I/O automata. Black-box testing amounts to checking whether an implementation conforms to a specification of its external behavior, by means of a set of tests derived solely from specification. The main problem is to derive a finite set of tests from a possibly infinite, dense time transition system representing the specification. The solution is to reduce the dense time transition system to an appropriate finite discrete subautomaton, the grid automaton, which contains enough information to completely represent the specification from a test perspective. Although the method results in a test suite of high exponential size and cannot be claimed to be of practical value, it gives the first algorithm that yields a finite and complete set of tests for dense real-time systems.

AB - We present a generalization of the classical theory of testing for Mealy machines to a setting of dense real-time systems. A model of timed I/O automata is introduced, inspired by the timed automaton model of Alur and Dill, together with a notion of test sequence for this model. Our main contributions is a test suite derivation algorithm for black-box conformance testing of timed I/O automata. Black-box testing amounts to checking whether an implementation conforms to a specification of its external behavior, by means of a set of tests derived solely from specification. The main problem is to derive a finite set of tests from a possibly infinite, dense time transition system representing the specification. The solution is to reduce the dense time transition system to an appropriate finite discrete subautomaton, the grid automaton, which contains enough information to completely represent the specification from a test perspective. Although the method results in a test suite of high exponential size and cannot be claimed to be of practical value, it gives the first algorithm that yields a finite and complete set of tests for dense real-time systems.

KW - FMT-RT: VERIFICATION OF REAL-TIME SYSTEMS

KW - METIS-204167

KW - IR-63254

KW - FMT-TESTING

KW - EWI-6371

U2 - 10.1016/S0304-3975(99)00134-6

DO - 10.1016/S0304-3975(99)00134-6

M3 - Article

VL - 254

SP - 225

EP - 257

JO - Theoretical computer science

JF - Theoretical computer science

SN - 0304-3975

IS - 1-2

M1 - 10.1016/S0304-3975(99)00134-6

ER -