Model-based testing of stochastically timed systems

Marcus Gerhold, Arnd Hartmanns* (Corresponding Author), Mariëlle Stoelinga

*Corresponding author for this work

    Research output: Contribution to journalArticleAcademicpeer-review

    13 Downloads (Pure)

    Abstract

    Many systems are inherently stochastic: they interact with unpredictable environments or use randomised algorithms. Classical model-based testing is insufficient for such systems: it only covers functional correctness. In this paper, we present two model-based testing frameworks that additionally cover the stochastic aspects in hard and soft real-time systems. Using the theory of Markov automata and stochastic automata for specifications, test cases, and a formal notion of conformance, they provide clean mechanisms to represent underspecification, randomisation, and stochastic timing. Markov automata provide a simple memoryless model of time, while stochastic automata support arbitrary continuous and discrete probability distributions. We cleanly define the theoretical foundations, outline practical algorithms for statistical conformance checking, and evaluate both frameworks’ capabilities by testing timing aspects of the Bluetooth device discovery protocol. We highlight the trade-off of simple and efficient statistical evaluation for Markov automata versus precise and realistic modelling with stochastic automata.
    Original languageEnglish
    Pages (from-to)207-233
    Number of pages27
    JournalInnovations in systems and software engineering
    Volume15
    Issue number3-4
    Early online date18 Jun 2019
    DOIs
    Publication statusPublished - Sep 2019

    Fingerprint

    Testing
    Bluetooth
    Real time systems
    Probability distributions
    Specifications
    Network protocols

    Keywords

    • UT-Hybrid-D

    Cite this

    @article{4b9442a19eb14100bf2fc1d95bd16813,
    title = "Model-based testing of stochastically timed systems",
    abstract = "Many systems are inherently stochastic: they interact with unpredictable environments or use randomised algorithms. Classical model-based testing is insufficient for such systems: it only covers functional correctness. In this paper, we present two model-based testing frameworks that additionally cover the stochastic aspects in hard and soft real-time systems. Using the theory of Markov automata and stochastic automata for specifications, test cases, and a formal notion of conformance, they provide clean mechanisms to represent underspecification, randomisation, and stochastic timing. Markov automata provide a simple memoryless model of time, while stochastic automata support arbitrary continuous and discrete probability distributions. We cleanly define the theoretical foundations, outline practical algorithms for statistical conformance checking, and evaluate both frameworks’ capabilities by testing timing aspects of the Bluetooth device discovery protocol. We highlight the trade-off of simple and efficient statistical evaluation for Markov automata versus precise and realistic modelling with stochastic automata.",
    keywords = "UT-Hybrid-D",
    author = "Marcus Gerhold and Arnd Hartmanns and Mari{\"e}lle Stoelinga",
    note = "Springer deal",
    year = "2019",
    month = "9",
    doi = "10.1007/s11334-019-00349-z",
    language = "English",
    volume = "15",
    pages = "207--233",
    journal = "Innovations in systems and software engineering",
    issn = "1614-5046",
    publisher = "Springer",
    number = "3-4",

    }

    Model-based testing of stochastically timed systems. / Gerhold, Marcus; Hartmanns, Arnd (Corresponding Author); Stoelinga, Mariëlle.

    In: Innovations in systems and software engineering, Vol. 15, No. 3-4, 09.2019, p. 207-233.

    Research output: Contribution to journalArticleAcademicpeer-review

    TY - JOUR

    T1 - Model-based testing of stochastically timed systems

    AU - Gerhold, Marcus

    AU - Hartmanns, Arnd

    AU - Stoelinga, Mariëlle

    N1 - Springer deal

    PY - 2019/9

    Y1 - 2019/9

    N2 - Many systems are inherently stochastic: they interact with unpredictable environments or use randomised algorithms. Classical model-based testing is insufficient for such systems: it only covers functional correctness. In this paper, we present two model-based testing frameworks that additionally cover the stochastic aspects in hard and soft real-time systems. Using the theory of Markov automata and stochastic automata for specifications, test cases, and a formal notion of conformance, they provide clean mechanisms to represent underspecification, randomisation, and stochastic timing. Markov automata provide a simple memoryless model of time, while stochastic automata support arbitrary continuous and discrete probability distributions. We cleanly define the theoretical foundations, outline practical algorithms for statistical conformance checking, and evaluate both frameworks’ capabilities by testing timing aspects of the Bluetooth device discovery protocol. We highlight the trade-off of simple and efficient statistical evaluation for Markov automata versus precise and realistic modelling with stochastic automata.

    AB - Many systems are inherently stochastic: they interact with unpredictable environments or use randomised algorithms. Classical model-based testing is insufficient for such systems: it only covers functional correctness. In this paper, we present two model-based testing frameworks that additionally cover the stochastic aspects in hard and soft real-time systems. Using the theory of Markov automata and stochastic automata for specifications, test cases, and a formal notion of conformance, they provide clean mechanisms to represent underspecification, randomisation, and stochastic timing. Markov automata provide a simple memoryless model of time, while stochastic automata support arbitrary continuous and discrete probability distributions. We cleanly define the theoretical foundations, outline practical algorithms for statistical conformance checking, and evaluate both frameworks’ capabilities by testing timing aspects of the Bluetooth device discovery protocol. We highlight the trade-off of simple and efficient statistical evaluation for Markov automata versus precise and realistic modelling with stochastic automata.

    KW - UT-Hybrid-D

    U2 - 10.1007/s11334-019-00349-z

    DO - 10.1007/s11334-019-00349-z

    M3 - Article

    VL - 15

    SP - 207

    EP - 233

    JO - Innovations in systems and software engineering

    JF - Innovations in systems and software engineering

    SN - 1614-5046

    IS - 3-4

    ER -