Divergent quiescent transition systems

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

    5 Citations (Scopus)
    62 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
    Title of host publicationProceedings of the 7th International Conference on Tests and Proofs (TAP 2013)
    EditorsMargus Veanes, Luca Viganò
    Place of PublicationBerlin
    PublisherSpringer
    Pages214-231
    Number of pages18
    ISBN (Print)978-3-642-38915-3
    DOIs
    Publication statusPublished - Jun 2013
    Event7th International Conference on Tests & Proofs 2013 - Budapest, Hungary
    Duration: 18 Jun 201319 Jun 2013
    Conference number: 7
    http://www.spacios.eu/TAP2013/

    Publication series

    NameLecture Notes in Computer Science
    PublisherSpringer Verlag
    Volume7942
    ISSN (Print)0302-9743
    ISSN (Electronic)1611-3349

    Conference

    Conference7th International Conference on Tests & Proofs 2013
    Abbreviated titleTAP 2013
    CountryHungary
    CityBudapest
    Period18/06/1319/06/13
    Internet address

    Keywords

    • EC Grant Agreement nr.: FP7/2007-2013
    • EC Grant Agreement nr.: FP7/318490
    • EWI-23427
    • Quiescence
    • IR-86479
    • IOCO
    • Divergence
    • METIS-297694
    • Model-Based Testing

    Cite this

    Stokkink, W. G. J., Timmer, M., & Stoelinga, M. I. A. (2013). Divergent quiescent transition systems. In M. Veanes, & L. Viganò (Eds.), Proceedings of the 7th International Conference on Tests and Proofs (TAP 2013) (pp. 214-231). (Lecture Notes in Computer Science; Vol. 7942). Berlin: Springer. https://doi.org/10.1007/978-3-642-38916-0_13
    Stokkink, W.G.J. ; Timmer, Mark ; Stoelinga, Mariëlle Ida Antoinette. / Divergent quiescent transition systems. Proceedings of the 7th International Conference on Tests and Proofs (TAP 2013). editor / Margus Veanes ; Luca Viganò. Berlin : Springer, 2013. pp. 214-231 (Lecture Notes in Computer Science).
    @inproceedings{aa41583600da43ed96cfce19b2b56d61,
    title = "Divergent quiescent transition systems",
    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 = "EC Grant Agreement nr.: FP7/2007-2013, EC Grant Agreement nr.: FP7/318490, EWI-23427, Quiescence, IR-86479, IOCO, Divergence, METIS-297694, Model-Based Testing",
    author = "W.G.J. Stokkink and Mark Timmer and Stoelinga, {Mari{\"e}lle Ida Antoinette}",
    note = "eemcs-eprint-23427",
    year = "2013",
    month = "6",
    doi = "10.1007/978-3-642-38916-0_13",
    language = "Undefined",
    isbn = "978-3-642-38915-3",
    series = "Lecture Notes in Computer Science",
    publisher = "Springer",
    pages = "214--231",
    editor = "Margus Veanes and Luca Vigan{\`o}",
    booktitle = "Proceedings of the 7th International Conference on Tests and Proofs (TAP 2013)",

    }

    Stokkink, WGJ, Timmer, M & Stoelinga, MIA 2013, Divergent quiescent transition systems. in M Veanes & L Viganò (eds), Proceedings of the 7th International Conference on Tests and Proofs (TAP 2013). Lecture Notes in Computer Science, vol. 7942, Springer, Berlin, pp. 214-231, 7th International Conference on Tests & Proofs 2013, Budapest, Hungary, 18/06/13. https://doi.org/10.1007/978-3-642-38916-0_13

    Divergent quiescent transition systems. / Stokkink, W.G.J.; Timmer, Mark; Stoelinga, Mariëlle Ida Antoinette.

    Proceedings of the 7th International Conference on Tests and Proofs (TAP 2013). ed. / Margus Veanes; Luca Viganò. Berlin : Springer, 2013. p. 214-231 (Lecture Notes in Computer Science; Vol. 7942).

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

    TY - GEN

    T1 - Divergent quiescent transition systems

    AU - Stokkink, W.G.J.

    AU - Timmer, Mark

    AU - Stoelinga, Mariëlle Ida Antoinette

    N1 - eemcs-eprint-23427

    PY - 2013/6

    Y1 - 2013/6

    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 - EC Grant Agreement nr.: FP7/2007-2013

    KW - EC Grant Agreement nr.: FP7/318490

    KW - EWI-23427

    KW - Quiescence

    KW - IR-86479

    KW - IOCO

    KW - Divergence

    KW - METIS-297694

    KW - Model-Based Testing

    U2 - 10.1007/978-3-642-38916-0_13

    DO - 10.1007/978-3-642-38916-0_13

    M3 - Conference contribution

    SN - 978-3-642-38915-3

    T3 - Lecture Notes in Computer Science

    SP - 214

    EP - 231

    BT - Proceedings of the 7th International Conference on Tests and Proofs (TAP 2013)

    A2 - Veanes, Margus

    A2 - Viganò, Luca

    PB - Springer

    CY - Berlin

    ER -

    Stokkink WGJ, Timmer M, Stoelinga MIA. Divergent quiescent transition systems. In Veanes M, Viganò L, editors, Proceedings of the 7th International Conference on Tests and Proofs (TAP 2013). Berlin: Springer. 2013. p. 214-231. (Lecture Notes in Computer Science). https://doi.org/10.1007/978-3-642-38916-0_13