Model-Based Testing for General Stochastic Time

    Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

    1 Citation (Scopus)
    80 Downloads (Pure)


    Many systems are inherently stochastic: they interact with unpredictable environments or use randomised algorithms. Then classical model-based testing is insufficient: it only covers functional correctness. In this paper, we present a new model-based testing framework that additionally covers the stochastic aspects in hard and soft real-time systems. Using the theory of stochastic automata for specifications, test cases and a formal notion of conformance, it provides clean mechanisms to represent underspecification, randomisation, and stochastic timing. Supporting arbitrary continuous and discrete probability distributions, the framework generalises previous work based on purely Markovian models. We cleanly define its theoretical foundations, and then outline a practical algorithm for statistical conformance testing based on the Kolmogorov-Smirnov test. We exemplify the framework’s capabilities and tradeoffs by testing timing aspects of the Bluetooth device discovery protocol.
    Original languageEnglish
    Title of host publicationProceedings of the 10th International NASA Formal Methods Symposium (NFM 2018)
    EditorsAaron Dutle, Cesar Munoz, Anthony Narkawicz
    ISBN (Electronic)978-3-319-77935-5
    ISBN (Print)978-3-319-77934-8
    Publication statusPublished - 11 Mar 2018
    Event10th International Symposium on NASA Formal Methods 2018 - Newport News Marriott at City Center, Newport News, United States
    Duration: 17 Apr 201819 Apr 2018
    Conference number: 10

    Publication series

    NameLecture Notes in Computer Science


    Conference10th International Symposium on NASA Formal Methods 2018
    Abbreviated titleNFM 2018
    CountryUnited States
    CityNewport News
    Internet address


    Dive into the research topics of 'Model-Based Testing for General Stochastic Time'. Together they form a unique fingerprint.

    Cite this