Fair Testing

Arend Rensink, W. Vogler

    Research output: Book/ReportReportProfessional

    21 Downloads (Pure)

    Abstract

    In this paper we present a solution to the long-standing problem of characterising the coarsest liveness-preserving pre-congruence with respect to a full (TCSP-inspired) process algebra. In fact, we present two distinct characterisations, which give rise to the same relation: an operational one based on a De Nicola-Hennessy-like testing modality which we call should-testing, and a denotational one based on a refined notion of failures. One of the distinguishing characteristics of the should-testing pre-congruence is that it abstracts from divergences in the same way as Milner’s observation congruence, and as a consequence is strictly coarser than observation congruence. In other words, should-testing has a built-in fairness assumption. This is in itself a property long sought-after; it is in notable contrast to the well-known must-testing of De Nicola and Hennessy (denotationally characterised by a combination of failures and divergences), which treats divergence as catrastrophic and hence is incompatible with observation congruence. Due to these characteristics, should-testing supports modular reasoning and allows to use the proof techniques of observation congruence, but also supports additional laws and techniques. Moreover, we show decidability of should-testing (on the basis of the denotational characterisation). Finally, we demonstrate its advantages by the application to a number of examples, including a scheduling problem, a version of the Alternating Bit-protocol, and fair lossy communication channels.
    Original languageUndefined
    Place of PublicationEnschede
    PublisherCentre for Telematics and Information Technology (CTIT)
    Number of pages74
    Publication statusPublished - Dec 2005

    Publication series

    NameCTIT Technical Report Series
    PublisherUniversity of Twente, Centre for Telematica and Information Technology (CTIT)
    No.05-64

    Keywords

    • Coarsest Congruence
    • EWI-6843
    • IR-54948
    • Process Algebra
    • Testing
    • Fairness
    • METIS-229702

    Cite this

    Rensink, A., & Vogler, W. (2005). Fair Testing. (CTIT Technical Report Series; No. 05-64). Enschede: Centre for Telematics and Information Technology (CTIT).
    Rensink, Arend ; Vogler, W. / Fair Testing. Enschede : Centre for Telematics and Information Technology (CTIT), 2005. 74 p. (CTIT Technical Report Series; 05-64).
    @book{f791acb864e44e05b2cd17e07f6eb9e3,
    title = "Fair Testing",
    abstract = "In this paper we present a solution to the long-standing problem of characterising the coarsest liveness-preserving pre-congruence with respect to a full (TCSP-inspired) process algebra. In fact, we present two distinct characterisations, which give rise to the same relation: an operational one based on a De Nicola-Hennessy-like testing modality which we call should-testing, and a denotational one based on a refined notion of failures. One of the distinguishing characteristics of the should-testing pre-congruence is that it abstracts from divergences in the same way as Milner’s observation congruence, and as a consequence is strictly coarser than observation congruence. In other words, should-testing has a built-in fairness assumption. This is in itself a property long sought-after; it is in notable contrast to the well-known must-testing of De Nicola and Hennessy (denotationally characterised by a combination of failures and divergences), which treats divergence as catrastrophic and hence is incompatible with observation congruence. Due to these characteristics, should-testing supports modular reasoning and allows to use the proof techniques of observation congruence, but also supports additional laws and techniques. Moreover, we show decidability of should-testing (on the basis of the denotational characterisation). Finally, we demonstrate its advantages by the application to a number of examples, including a scheduling problem, a version of the Alternating Bit-protocol, and fair lossy communication channels.",
    keywords = "Coarsest Congruence, EWI-6843, IR-54948, Process Algebra, Testing, Fairness, METIS-229702",
    author = "Arend Rensink and W. Vogler",
    note = "RensinkVog2005 Report nr. 05-64",
    year = "2005",
    month = "12",
    language = "Undefined",
    series = "CTIT Technical Report Series",
    publisher = "Centre for Telematics and Information Technology (CTIT)",
    number = "05-64",
    address = "Netherlands",

    }

    Rensink, A & Vogler, W 2005, Fair Testing. CTIT Technical Report Series, no. 05-64, Centre for Telematics and Information Technology (CTIT), Enschede.

    Fair Testing. / Rensink, Arend; Vogler, W.

    Enschede : Centre for Telematics and Information Technology (CTIT), 2005. 74 p. (CTIT Technical Report Series; No. 05-64).

    Research output: Book/ReportReportProfessional

    TY - BOOK

    T1 - Fair Testing

    AU - Rensink, Arend

    AU - Vogler, W.

    N1 - RensinkVog2005 Report nr. 05-64

    PY - 2005/12

    Y1 - 2005/12

    N2 - In this paper we present a solution to the long-standing problem of characterising the coarsest liveness-preserving pre-congruence with respect to a full (TCSP-inspired) process algebra. In fact, we present two distinct characterisations, which give rise to the same relation: an operational one based on a De Nicola-Hennessy-like testing modality which we call should-testing, and a denotational one based on a refined notion of failures. One of the distinguishing characteristics of the should-testing pre-congruence is that it abstracts from divergences in the same way as Milner’s observation congruence, and as a consequence is strictly coarser than observation congruence. In other words, should-testing has a built-in fairness assumption. This is in itself a property long sought-after; it is in notable contrast to the well-known must-testing of De Nicola and Hennessy (denotationally characterised by a combination of failures and divergences), which treats divergence as catrastrophic and hence is incompatible with observation congruence. Due to these characteristics, should-testing supports modular reasoning and allows to use the proof techniques of observation congruence, but also supports additional laws and techniques. Moreover, we show decidability of should-testing (on the basis of the denotational characterisation). Finally, we demonstrate its advantages by the application to a number of examples, including a scheduling problem, a version of the Alternating Bit-protocol, and fair lossy communication channels.

    AB - In this paper we present a solution to the long-standing problem of characterising the coarsest liveness-preserving pre-congruence with respect to a full (TCSP-inspired) process algebra. In fact, we present two distinct characterisations, which give rise to the same relation: an operational one based on a De Nicola-Hennessy-like testing modality which we call should-testing, and a denotational one based on a refined notion of failures. One of the distinguishing characteristics of the should-testing pre-congruence is that it abstracts from divergences in the same way as Milner’s observation congruence, and as a consequence is strictly coarser than observation congruence. In other words, should-testing has a built-in fairness assumption. This is in itself a property long sought-after; it is in notable contrast to the well-known must-testing of De Nicola and Hennessy (denotationally characterised by a combination of failures and divergences), which treats divergence as catrastrophic and hence is incompatible with observation congruence. Due to these characteristics, should-testing supports modular reasoning and allows to use the proof techniques of observation congruence, but also supports additional laws and techniques. Moreover, we show decidability of should-testing (on the basis of the denotational characterisation). Finally, we demonstrate its advantages by the application to a number of examples, including a scheduling problem, a version of the Alternating Bit-protocol, and fair lossy communication channels.

    KW - Coarsest Congruence

    KW - EWI-6843

    KW - IR-54948

    KW - Process Algebra

    KW - Testing

    KW - Fairness

    KW - METIS-229702

    M3 - Report

    T3 - CTIT Technical Report Series

    BT - Fair Testing

    PB - Centre for Telematics and Information Technology (CTIT)

    CY - Enschede

    ER -

    Rensink A, Vogler W. Fair Testing. Enschede: Centre for Telematics and Information Technology (CTIT), 2005. 74 p. (CTIT Technical Report Series; 05-64).