Bounded determinization of timed automata with silent transitions

Florian Lukas Lorber, Amnon Rosenmann, Dejan Nickovic, Bernhard Aichernig

Publikation: Beitrag in einer FachzeitschriftArtikelForschungBegutachtung

Abstract

Deterministic timed automata are strictly less expressive than their non-deterministic counterparts, which are again less expressive than those with silent transitions. As a consequence, timed automata are in general non-determinizable. This is unfortunate since deterministic automata play a major role in model-based testing, observability and implementability. However, by bounding the length of the traces in the automaton, effective determinization becomes possible. We propose a novel procedure for bounded determinization of timed automata. The procedure unfolds the automata to bounded trees, removes all silent transitions and determinizes via disjunction of guards. The proposed algorithms are optimized to the bounded setting and thus are more efficient and can handle a larger class of timed automata than the general algorithms. We show how to apply the approach in a fault-based test-case generation method, called model-based mutation testing, that was previously restricted to deterministic timed automata. The approach is implemented in a prototype tool and evaluated on several scientific examples and one industrial case study. To our best knowledge, this is the first implementation of this type of procedure for timed automata.
Originalspracheenglisch
Seiten (von - bis)291–326
FachzeitschriftReal-time systems
Jahrgang53
Ausgabenummer3
DOIs
PublikationsstatusVeröffentlicht - Mai 2017

Fingerprint

Timed Automata
Observability
Testing
Automata
Model-based Testing
Mutation
Fault
Strictly
Trace
Prototype
Model-based

Schlagwörter

    Dies zitieren

    Bounded determinization of timed automata with silent transitions. / Lorber, Florian Lukas; Rosenmann, Amnon; Nickovic, Dejan; Aichernig, Bernhard.

    in: Real-time systems, Jahrgang 53, Nr. 3, 05.2017, S. 291–326.

    Publikation: Beitrag in einer FachzeitschriftArtikelForschungBegutachtung

    Lorber, Florian Lukas ; Rosenmann, Amnon ; Nickovic, Dejan ; Aichernig, Bernhard. / Bounded determinization of timed automata with silent transitions. in: Real-time systems. 2017 ; Jahrgang 53, Nr. 3. S. 291–326.
    @article{69e528a6e9bb4910a1d1d3788f2447cd,
    title = "Bounded determinization of timed automata with silent transitions",
    abstract = "Deterministic timed automata are strictly less expressive than their non-deterministic counterparts, which are again less expressive than those with silent transitions. As a consequence, timed automata are in general non-determinizable. This is unfortunate since deterministic automata play a major role in model-based testing, observability and implementability. However, by bounding the length of the traces in the automaton, effective determinization becomes possible. We propose a novel procedure for bounded determinization of timed automata. The procedure unfolds the automata to bounded trees, removes all silent transitions and determinizes via disjunction of guards. The proposed algorithms are optimized to the bounded setting and thus are more efficient and can handle a larger class of timed automata than the general algorithms. We show how to apply the approach in a fault-based test-case generation method, called model-based mutation testing, that was previously restricted to deterministic timed automata. The approach is implemented in a prototype tool and evaluated on several scientific examples and one industrial case study. To our best knowledge, this is the first implementation of this type of procedure for timed automata.",
    keywords = "Timed automata, Determinization, Silent transition removal, Diagonal constraints, Testcase generation, Model-based testing, nodel-based mutation testing",
    author = "Lorber, {Florian Lukas} and Amnon Rosenmann and Dejan Nickovic and Bernhard Aichernig",
    year = "2017",
    month = "5",
    doi = "https://doi.org/10.1007/s11241-017-9271-x",
    language = "English",
    volume = "53",
    pages = "291–326",
    journal = "Real-time systems",
    issn = "0922-6443",
    publisher = "Springer Netherlands",
    number = "3",

    }

    TY - JOUR

    T1 - Bounded determinization of timed automata with silent transitions

    AU - Lorber, Florian Lukas

    AU - Rosenmann, Amnon

    AU - Nickovic, Dejan

    AU - Aichernig, Bernhard

    PY - 2017/5

    Y1 - 2017/5

    N2 - Deterministic timed automata are strictly less expressive than their non-deterministic counterparts, which are again less expressive than those with silent transitions. As a consequence, timed automata are in general non-determinizable. This is unfortunate since deterministic automata play a major role in model-based testing, observability and implementability. However, by bounding the length of the traces in the automaton, effective determinization becomes possible. We propose a novel procedure for bounded determinization of timed automata. The procedure unfolds the automata to bounded trees, removes all silent transitions and determinizes via disjunction of guards. The proposed algorithms are optimized to the bounded setting and thus are more efficient and can handle a larger class of timed automata than the general algorithms. We show how to apply the approach in a fault-based test-case generation method, called model-based mutation testing, that was previously restricted to deterministic timed automata. The approach is implemented in a prototype tool and evaluated on several scientific examples and one industrial case study. To our best knowledge, this is the first implementation of this type of procedure for timed automata.

    AB - Deterministic timed automata are strictly less expressive than their non-deterministic counterparts, which are again less expressive than those with silent transitions. As a consequence, timed automata are in general non-determinizable. This is unfortunate since deterministic automata play a major role in model-based testing, observability and implementability. However, by bounding the length of the traces in the automaton, effective determinization becomes possible. We propose a novel procedure for bounded determinization of timed automata. The procedure unfolds the automata to bounded trees, removes all silent transitions and determinizes via disjunction of guards. The proposed algorithms are optimized to the bounded setting and thus are more efficient and can handle a larger class of timed automata than the general algorithms. We show how to apply the approach in a fault-based test-case generation method, called model-based mutation testing, that was previously restricted to deterministic timed automata. The approach is implemented in a prototype tool and evaluated on several scientific examples and one industrial case study. To our best knowledge, this is the first implementation of this type of procedure for timed automata.

    KW - Timed automata

    KW - Determinization

    KW - Silent transition removal

    KW - Diagonal constraints

    KW - Testcase generation

    KW - Model-based testing

    KW - nodel-based mutation testing

    U2 - https://doi.org/10.1007/s11241-017-9271-x

    DO - https://doi.org/10.1007/s11241-017-9271-x

    M3 - Article

    VL - 53

    SP - 291

    EP - 326

    JO - Real-time systems

    JF - Real-time systems

    SN - 0922-6443

    IS - 3

    ER -