Testing Timed Automata

Jan Springintveld, Frits Vaandrager, P.R. d' Argenio

    Research output: Contribution to journalArticleAcademic

    186 Citations (Scopus)

    Abstract

    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.
    Original languageUndefined
    Article number10.1016/S0304-3975(99)00134-6
    Pages (from-to)225-257
    Number of pages33
    JournalTheoretical computer science
    Volume254
    Issue number1-2
    DOIs
    Publication statusPublished - 2001

    Keywords

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

    Cite this

    Springintveld, J., Vaandrager, F., & d' Argenio, P. R. (2001). Testing Timed Automata. 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
    Springintveld, Jan ; Vaandrager, Frits ; d' Argenio, P.R. / Testing Timed Automata. In: Theoretical computer science. 2001 ; Vol. 254, No. 1-2. pp. 225-257.
    @article{10826dc1d0774ab2988669e6443bf8fb,
    title = "Testing Timed Automata",
    abstract = "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.",
    keywords = "FMT-RT: VERIFICATION OF REAL-TIME SYSTEMS, METIS-204167, IR-63254, FMT-TESTING, EWI-6371",
    author = "Jan Springintveld and Frits Vaandrager and {d' Argenio}, P.R.",
    year = "2001",
    doi = "10.1016/S0304-3975(99)00134-6",
    language = "Undefined",
    volume = "254",
    pages = "225--257",
    journal = "Theoretical computer science",
    issn = "0304-3975",
    publisher = "Elsevier",
    number = "1-2",

    }

    Springintveld, J, Vaandrager, F & d' Argenio, PR 2001, 'Testing Timed Automata', 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.

    In: Theoretical computer science, Vol. 254, No. 1-2, 10.1016/S0304-3975(99)00134-6, 2001, p. 225-257.

    Research output: Contribution to journalArticleAcademic

    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 -

    Springintveld J, Vaandrager F, d' Argenio PR. Testing Timed Automata. Theoretical computer science. 2001;254(1-2):225-257. 10.1016/S0304-3975(99)00134-6. https://doi.org/10.1016/S0304-3975(99)00134-6