On the coverage of Partial Validations

Ed Brinksma

    Research output: Chapter in Book/Report/Conference proceeding › Chapter › Academic

    Abstract

    The validation of implementations is an essential part of the design of both hardware and software systems in order to establish the correctness of such systems. As such it has been an important application area for all kinds of formal methods to support this activity. Many of such methods, however, aim at a complete proof of correctness, which become unmanageable in the case of larger, realistic designs. In practice, therefore, attention is limited to such methods that can be applied partially or in an approximative manner. Albeit more pragmatic, these approaches usually lack a good measure for the extent to which correctness is established. Such coverage measures are needed to compare and assess different strategies for partial validation in the context of a given specification. In this article we propose to follow a measure-theoretic approach in which an exogenous cost function (quantifying the effect of certain properties in an implementation) is integrated over a measure that is induced by the probability of error occurrences in implementations. In this way, in fact, we do not only obtain a notion of coverage, but a general way of assigning measures to specification theories in the context of a given class of implementation structures.
    Original languageEnglish
    Title of host publicationAlgebraic Methodology and Software Technology (AMAST’93)
    Subtitle of host publicationProceedings of the Third International Conference, University of Twente, Enschede, The Netherlands 21–25 June 1993
    Place of PublicationLondon
    PublisherSpringer
    Pages245-252
    ISBN (Electronic)978-1-4471-3227-1
    ISBN (Print)978-3-540-19852-9
    DOIs
    Publication statusPublished - 1993
    Event3rd International Conference on Algebraic Methodology and Software Engineering, AMAST 1993 - Universiteit Twente, Enschede
    Duration: 21 Jun 1993 → 25 Jun 1993
    Conference number: 3

    Publication series

    NameWorkshops in Computing
    PublisherSpringer
    ISSN (Print)1431-1682

    Conference

    Conference3rd International Conference on Algebraic Methodology and Software Engineering, AMAST 1993
    Abbreviated titleAMAST
    CityEnschede
    Period21/06/93 → 25/06/93

    Fingerprint

    Specifications
    Formal methods
    Cost functions
    Hardware

    Cite this

    Brinksma, E. (1993). On the coverage of Partial Validations. In Algebraic Methodology and Software Technology (AMAST’93): Proceedings of the Third International Conference, University of Twente, Enschede, The Netherlands 21–25 June 1993 (pp. 245-252). (Workshops in Computing). London: Springer. https://doi.org/10.1007/978-1-4471-3227-1_25
    Brinksma, Ed. / On the coverage of Partial Validations. Algebraic Methodology and Software Technology (AMAST’93): Proceedings of the Third International Conference, University of Twente, Enschede, The Netherlands 21–25 June 1993. London : Springer, 1993. pp. 245-252 (Workshops in Computing).
    @inbook{65dda290bd7a4cb5b216cb0d4c3af925,
    title = "On the coverage of Partial Validations",
    abstract = "The validation of implementations is an essential part of the design of both hardware and software systems in order to establish the correctness of such systems. As such it has been an important application area for all kinds of formal methods to support this activity. Many of such methods, however, aim at a complete proof of correctness, which become unmanageable in the case of larger, realistic designs. In practice, therefore, attention is limited to such methods that can be applied partially or in an approximative manner. Albeit more pragmatic, these approaches usually lack a good measure for the extent to which correctness is established. Such coverage measures are needed to compare and assess different strategies for partial validation in the context of a given specification. In this article we propose to follow a measure-theoretic approach in which an exogenous cost function (quantifying the effect of certain properties in an implementation) is integrated over a measure that is induced by the probability of error occurrences in implementations. In this way, in fact, we do not only obtain a notion of coverage, but a general way of assigning measures to specification theories in the context of a given class of implementation structures.",
    author = "Ed Brinksma",
    year = "1993",
    doi = "10.1007/978-1-4471-3227-1_25",
    language = "English",
    isbn = "978-3-540-19852-9",
    series = "Workshops in Computing",
    publisher = "Springer",
    pages = "245--252",
    booktitle = "Algebraic Methodology and Software Technology (AMAST’93)",

    }

    Brinksma, E 1993, On the coverage of Partial Validations. in Algebraic Methodology and Software Technology (AMAST’93): Proceedings of the Third International Conference, University of Twente, Enschede, The Netherlands 21–25 June 1993. Workshops in Computing, Springer, London, pp. 245-252, 3rd International Conference on Algebraic Methodology and Software Engineering, AMAST 1993, Enschede, 21/06/93. https://doi.org/10.1007/978-1-4471-3227-1_25

    On the coverage of Partial Validations. / Brinksma, Ed.

    Algebraic Methodology and Software Technology (AMAST’93): Proceedings of the Third International Conference, University of Twente, Enschede, The Netherlands 21–25 June 1993. London : Springer, 1993. p. 245-252 (Workshops in Computing).

    Research output: Chapter in Book/Report/Conference proceeding › Chapter › Academic

    TY - CHAP

    T1 - On the coverage of Partial Validations

    AU - Brinksma, Ed

    PY - 1993

    Y1 - 1993

    N2 - The validation of implementations is an essential part of the design of both hardware and software systems in order to establish the correctness of such systems. As such it has been an important application area for all kinds of formal methods to support this activity. Many of such methods, however, aim at a complete proof of correctness, which become unmanageable in the case of larger, realistic designs. In practice, therefore, attention is limited to such methods that can be applied partially or in an approximative manner. Albeit more pragmatic, these approaches usually lack a good measure for the extent to which correctness is established. Such coverage measures are needed to compare and assess different strategies for partial validation in the context of a given specification. In this article we propose to follow a measure-theoretic approach in which an exogenous cost function (quantifying the effect of certain properties in an implementation) is integrated over a measure that is induced by the probability of error occurrences in implementations. In this way, in fact, we do not only obtain a notion of coverage, but a general way of assigning measures to specification theories in the context of a given class of implementation structures.

    AB - The validation of implementations is an essential part of the design of both hardware and software systems in order to establish the correctness of such systems. As such it has been an important application area for all kinds of formal methods to support this activity. Many of such methods, however, aim at a complete proof of correctness, which become unmanageable in the case of larger, realistic designs. In practice, therefore, attention is limited to such methods that can be applied partially or in an approximative manner. Albeit more pragmatic, these approaches usually lack a good measure for the extent to which correctness is established. Such coverage measures are needed to compare and assess different strategies for partial validation in the context of a given specification. In this article we propose to follow a measure-theoretic approach in which an exogenous cost function (quantifying the effect of certain properties in an implementation) is integrated over a measure that is induced by the probability of error occurrences in implementations. In this way, in fact, we do not only obtain a notion of coverage, but a general way of assigning measures to specification theories in the context of a given class of implementation structures.

    U2 - 10.1007/978-1-4471-3227-1_25

    DO - 10.1007/978-1-4471-3227-1_25

    M3 - Chapter

    SN - 978-3-540-19852-9

    T3 - Workshops in Computing

    SP - 245

    EP - 252

    BT - Algebraic Methodology and Software Technology (AMAST’93)

    PB - Springer

    CY - London

    ER -

    Brinksma E. On the coverage of Partial Validations. In Algebraic Methodology and Software Technology (AMAST’93): Proceedings of the Third International Conference, University of Twente, Enschede, The Netherlands 21–25 June 1993. London: Springer. 1993. p. 245-252. (Workshops in Computing). https://doi.org/10.1007/978-1-4471-3227-1_25

    Access to Document