Divergent Quiescent Transition Systems (extended version)

    Research output: Book/ReportReportAcademic

    14 Downloads (Pure)

    Abstract

    Quiescence is a fundamental concept in modelling system behaviour, as it explicitly represents the fact that no output is produced in certain states. The notion of quiescence is also essential to model-based testing: if a particular implementation under test does not provide any output, then the test evaluation algorithm must decide whether or not to allow this behaviour. To explicitly model quiescence in all its glory, we introduce Divergent Quiescent Transition Systems (DQTSs). DQTSs model quiescence using explicit delta-labelled transitions, analogous to Suspension Automata (SAs) in the well-known ioco framework. Whereas SAs have only been defined implicitly, DQTSs for the first time provide a fully-formalised framework for quiescence. Also, while SAs are restricted to convergent systems (i.e., without tau-cycles), we show how quiescence can be treated naturally using a notion of fairness, allowing systems exhibiting divergence to be modelled as well. We study compositionality under the familiar automata-theoretical operations of determinisation, parallel composition and action hiding. We provide a non-trivial algorithm for detecting divergent states, and discuss its complexity. Finally, we show how to use DQTSs in the context of model-based testing, for the first time presenting a full-fledged theory that allows ioco to be applied to divergent systems.
    Original languageUndefined
    Place of PublicationEnschede
    PublisherCentre for Telematics and Information Technology (CTIT)
    Number of pages39
    Publication statusPublished - Mar 2013

    Publication series

    NameCTIT Technical Report Series
    PublisherUniversity of Twente, Centre for Telematica and Information Technology (CTIT)
    No.TR-CTIT-13-08
    ISSN (Print)1381-3625

    Keywords

    • IR-85339
    • METIS-296384
    • EWI-23233
    • EC Grant Agreement nr.: FP7/2007-2013
    • EC Grant Agreement nr.: FP7/318490

    Cite this

    Stokkink, W. G. J., Timmer, M., & Stoelinga, M. I. A. (2013). Divergent Quiescent Transition Systems (extended version). (CTIT Technical Report Series; No. TR-CTIT-13-08). Enschede: Centre for Telematics and Information Technology (CTIT).
    Stokkink, W.G.J. ; Timmer, Mark ; Stoelinga, Mariëlle Ida Antoinette. / Divergent Quiescent Transition Systems (extended version). Enschede : Centre for Telematics and Information Technology (CTIT), 2013. 39 p. (CTIT Technical Report Series; TR-CTIT-13-08).
    @book{bfc99bf8a3a84d4a9de0d89539fc3084,
    title = "Divergent Quiescent Transition Systems (extended version)",
    abstract = "Quiescence is a fundamental concept in modelling system behaviour, as it explicitly represents the fact that no output is produced in certain states. The notion of quiescence is also essential to model-based testing: if a particular implementation under test does not provide any output, then the test evaluation algorithm must decide whether or not to allow this behaviour. To explicitly model quiescence in all its glory, we introduce Divergent Quiescent Transition Systems (DQTSs). DQTSs model quiescence using explicit delta-labelled transitions, analogous to Suspension Automata (SAs) in the well-known ioco framework. Whereas SAs have only been defined implicitly, DQTSs for the first time provide a fully-formalised framework for quiescence. Also, while SAs are restricted to convergent systems (i.e., without tau-cycles), we show how quiescence can be treated naturally using a notion of fairness, allowing systems exhibiting divergence to be modelled as well. We study compositionality under the familiar automata-theoretical operations of determinisation, parallel composition and action hiding. We provide a non-trivial algorithm for detecting divergent states, and discuss its complexity. Finally, we show how to use DQTSs in the context of model-based testing, for the first time presenting a full-fledged theory that allows ioco to be applied to divergent systems.",
    keywords = "IR-85339, METIS-296384, EWI-23233, EC Grant Agreement nr.: FP7/2007-2013, EC Grant Agreement nr.: FP7/318490",
    author = "W.G.J. Stokkink and Mark Timmer and Stoelinga, {Mari{\"e}lle Ida Antoinette}",
    note = "eemcs-eprint-23233",
    year = "2013",
    month = "3",
    language = "Undefined",
    series = "CTIT Technical Report Series",
    publisher = "Centre for Telematics and Information Technology (CTIT)",
    number = "TR-CTIT-13-08",
    address = "Netherlands",

    }

    Stokkink, WGJ, Timmer, M & Stoelinga, MIA 2013, Divergent Quiescent Transition Systems (extended version). CTIT Technical Report Series, no. TR-CTIT-13-08, Centre for Telematics and Information Technology (CTIT), Enschede.

    Divergent Quiescent Transition Systems (extended version). / Stokkink, W.G.J.; Timmer, Mark; Stoelinga, Mariëlle Ida Antoinette.

    Enschede : Centre for Telematics and Information Technology (CTIT), 2013. 39 p. (CTIT Technical Report Series; No. TR-CTIT-13-08).

    Research output: Book/ReportReportAcademic

    TY - BOOK

    T1 - Divergent Quiescent Transition Systems (extended version)

    AU - Stokkink, W.G.J.

    AU - Timmer, Mark

    AU - Stoelinga, Mariëlle Ida Antoinette

    N1 - eemcs-eprint-23233

    PY - 2013/3

    Y1 - 2013/3

    N2 - Quiescence is a fundamental concept in modelling system behaviour, as it explicitly represents the fact that no output is produced in certain states. The notion of quiescence is also essential to model-based testing: if a particular implementation under test does not provide any output, then the test evaluation algorithm must decide whether or not to allow this behaviour. To explicitly model quiescence in all its glory, we introduce Divergent Quiescent Transition Systems (DQTSs). DQTSs model quiescence using explicit delta-labelled transitions, analogous to Suspension Automata (SAs) in the well-known ioco framework. Whereas SAs have only been defined implicitly, DQTSs for the first time provide a fully-formalised framework for quiescence. Also, while SAs are restricted to convergent systems (i.e., without tau-cycles), we show how quiescence can be treated naturally using a notion of fairness, allowing systems exhibiting divergence to be modelled as well. We study compositionality under the familiar automata-theoretical operations of determinisation, parallel composition and action hiding. We provide a non-trivial algorithm for detecting divergent states, and discuss its complexity. Finally, we show how to use DQTSs in the context of model-based testing, for the first time presenting a full-fledged theory that allows ioco to be applied to divergent systems.

    AB - Quiescence is a fundamental concept in modelling system behaviour, as it explicitly represents the fact that no output is produced in certain states. The notion of quiescence is also essential to model-based testing: if a particular implementation under test does not provide any output, then the test evaluation algorithm must decide whether or not to allow this behaviour. To explicitly model quiescence in all its glory, we introduce Divergent Quiescent Transition Systems (DQTSs). DQTSs model quiescence using explicit delta-labelled transitions, analogous to Suspension Automata (SAs) in the well-known ioco framework. Whereas SAs have only been defined implicitly, DQTSs for the first time provide a fully-formalised framework for quiescence. Also, while SAs are restricted to convergent systems (i.e., without tau-cycles), we show how quiescence can be treated naturally using a notion of fairness, allowing systems exhibiting divergence to be modelled as well. We study compositionality under the familiar automata-theoretical operations of determinisation, parallel composition and action hiding. We provide a non-trivial algorithm for detecting divergent states, and discuss its complexity. Finally, we show how to use DQTSs in the context of model-based testing, for the first time presenting a full-fledged theory that allows ioco to be applied to divergent systems.

    KW - IR-85339

    KW - METIS-296384

    KW - EWI-23233

    KW - EC Grant Agreement nr.: FP7/2007-2013

    KW - EC Grant Agreement nr.: FP7/318490

    M3 - Report

    T3 - CTIT Technical Report Series

    BT - Divergent Quiescent Transition Systems (extended version)

    PB - Centre for Telematics and Information Technology (CTIT)

    CY - Enschede

    ER -

    Stokkink WGJ, Timmer M, Stoelinga MIA. Divergent Quiescent Transition Systems (extended version). Enschede: Centre for Telematics and Information Technology (CTIT), 2013. 39 p. (CTIT Technical Report Series; TR-CTIT-13-08).