On the coverage of Partial Validations

Ed Brinksma

doi:10.1007/978-1-4471-3227-1_25

On the coverage of Partial Validations

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 language	English
Title of host publication	Algebraic Methodology and Software Technology (AMAST’93)
Subtitle of host publication	Proceedings of the Third International Conference, University of Twente, Enschede, The Netherlands 21–25 June 1993
Place of Publication	London
Publisher	Springer
Pages	245-252
ISBN (Electronic)	978-1-4471-3227-1
ISBN (Print)	978-3-540-19852-9
DOIs	https://doi.org/10.1007/978-1-4471-3227-1_25
Publication status	Published - 1993
Event	3rd 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

Name	Workshops in Computing
Publisher	Springer
ISSN (Print)	1431-1682

Conference

Conference	3rd International Conference on Algebraic Methodology and Software Engineering, AMAST 1993
Abbreviated title	AMAST
City	Enschede
Period	21/06/93 → 25/06/93

Access to Document

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

Fingerprint Dive into the research topics of 'On the coverage of Partial Validations'. Together they form a unique fingerprint.

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

@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 -