On Combining Functional Verification and Performance Evaluation Using CADP

Hubert Garavel; Holger Hermanns

doi:10.1007/3-540-45614-7_23

On Combining Functional Verification and Performance Evaluation Using CADP

Hubert Garavel, Holger Hermanns

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

31 Citations (Scopus)

12 Downloads (Pure)

Abstract

Considering functional correctness and performance evaluation in a common framework is desirable, both for scientific and economic reasons. In this paper, we describe how the CADP toolbox, originally designed for verifying the functional correctness of LOTOS specifications, can also be used for performance evaluation. We illustrate the proposed approach by the performance study of the SCSI-2 bus arbitration protocol.

Original language	English
Title of host publication	FME 2002: Formal Methods - Getting IT Right
Subtitle of host publication	International Symposium of Formal Methods Europe Copenhagen, Denmark, July 22–24, 2002: Proceedings
Editors	Lars-Henrik Eriksson, Peter Alexander Lindsay
Place of Publication	Berlin, Heidelberg
Publisher	Springer
Pages	410-429
Number of pages	20
ISBN (Electronic)	978-3-540-45614-8
ISBN (Print)	978-3-540-43928-8
DOIs	https://doi.org/10.1007/3-540-45614-7_23
Publication status	Published - 2002
Event	Formal Methods - Getting IT Right, FME 2002: 11th International Symposium of Formal Methods Europe - Copenhagen, Denmark Duration: 22 Jul 2002 → 24 Jul 2002 Conference number: 11

Publication series

Name	Lecture Notes in Computer Science
Publisher	Springer
Volume	2391
ISSN (Print)	0302-9743

Conference

Conference	Formal Methods - Getting IT Right, FME 2002
Abbreviated title	FME
Country	Denmark
City	Copenhagen
Period	22/07/02 → 24/07/02

Keywords

Label transition system
Process algebra
Functional correctness
Delay transition
Strong bisimulation

Access to Document

10.1007/3-540-45614-7_23

Fingerprint Dive into the research topics of 'On Combining Functional Verification and Performance Evaluation Using CADP'. Together they form a unique fingerprint.

Cite this

Garavel, H., & Hermanns, H. (2002). On Combining Functional Verification and Performance Evaluation Using CADP. In L-H. Eriksson, & P. A. Lindsay (Eds.), FME 2002: Formal Methods - Getting IT Right: International Symposium of Formal Methods Europe Copenhagen, Denmark, July 22–24, 2002: Proceedings (pp. 410-429). (Lecture Notes in Computer Science; Vol. 2391). Springer. https://doi.org/10.1007/3-540-45614-7_23

Garavel, Hubert ; Hermanns, Holger. / On Combining Functional Verification and Performance Evaluation Using CADP. FME 2002: Formal Methods - Getting IT Right: International Symposium of Formal Methods Europe Copenhagen, Denmark, July 22–24, 2002: Proceedings. editor / Lars-Henrik Eriksson ; Peter Alexander Lindsay. Berlin, Heidelberg : Springer, 2002. pp. 410-429 (Lecture Notes in Computer Science).

@inproceedings{5eae502c092b4e39acd38c204215997c,

title = "On Combining Functional Verification and Performance Evaluation Using CADP",

abstract = "Considering functional correctness and performance evaluation in a common framework is desirable, both for scientific and economic reasons. In this paper, we describe how the CADP toolbox, originally designed for verifying the functional correctness of LOTOS specifications, can also be used for performance evaluation. We illustrate the proposed approach by the performance study of the SCSI-2 bus arbitration protocol.",

keywords = "Label transition system, Process algebra, Functional correctness, Delay transition, Strong bisimulation",

author = "Hubert Garavel and Holger Hermanns",

year = "2002",

doi = "10.1007/3-540-45614-7_23",

language = "English",

isbn = "978-3-540-43928-8",

series = "Lecture Notes in Computer Science",

publisher = "Springer",

pages = "410--429",

editor = "Lars-Henrik Eriksson and Lindsay, {Peter Alexander}",

booktitle = "FME 2002: Formal Methods - Getting IT Right",

note = "Formal Methods - Getting IT Right, FME 2002 : 11th International Symposium of Formal Methods Europe, FME ; Conference date: 22-07-2002 Through 24-07-2002",

}

Garavel, H & Hermanns, H 2002, On Combining Functional Verification and Performance Evaluation Using CADP. in L-H Eriksson & PA Lindsay (eds), FME 2002: Formal Methods - Getting IT Right: International Symposium of Formal Methods Europe Copenhagen, Denmark, July 22–24, 2002: Proceedings. Lecture Notes in Computer Science, vol. 2391, Springer, Berlin, Heidelberg, pp. 410-429, Formal Methods - Getting IT Right, FME 2002, Copenhagen, Denmark, 22/07/02. https://doi.org/10.1007/3-540-45614-7_23

On Combining Functional Verification and Performance Evaluation Using CADP. / Garavel, Hubert; Hermanns, Holger.

FME 2002: Formal Methods - Getting IT Right: International Symposium of Formal Methods Europe Copenhagen, Denmark, July 22–24, 2002: Proceedings. ed. / Lars-Henrik Eriksson; Peter Alexander Lindsay. Berlin, Heidelberg : Springer, 2002. p. 410-429 (Lecture Notes in Computer Science; Vol. 2391).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

TY - GEN

T1 - On Combining Functional Verification and Performance Evaluation Using CADP

AU - Garavel, Hubert

AU - Hermanns, Holger

N1 - Conference code: 11

PY - 2002

Y1 - 2002

N2 - Considering functional correctness and performance evaluation in a common framework is desirable, both for scientific and economic reasons. In this paper, we describe how the CADP toolbox, originally designed for verifying the functional correctness of LOTOS specifications, can also be used for performance evaluation. We illustrate the proposed approach by the performance study of the SCSI-2 bus arbitration protocol.

AB - Considering functional correctness and performance evaluation in a common framework is desirable, both for scientific and economic reasons. In this paper, we describe how the CADP toolbox, originally designed for verifying the functional correctness of LOTOS specifications, can also be used for performance evaluation. We illustrate the proposed approach by the performance study of the SCSI-2 bus arbitration protocol.

KW - Label transition system

KW - Process algebra

KW - Functional correctness

KW - Delay transition

KW - Strong bisimulation

U2 - 10.1007/3-540-45614-7_23

DO - 10.1007/3-540-45614-7_23

M3 - Conference contribution

SN - 978-3-540-43928-8

T3 - Lecture Notes in Computer Science

SP - 410

EP - 429

BT - FME 2002: Formal Methods - Getting IT Right

A2 - Eriksson, Lars-Henrik

A2 - Lindsay, Peter Alexander

PB - Springer

CY - Berlin, Heidelberg

T2 - Formal Methods - Getting IT Right, FME 2002

Y2 - 22 July 2002 through 24 July 2002

ER -

Garavel H, Hermanns H. On Combining Functional Verification and Performance Evaluation Using CADP. In Eriksson L-H, Lindsay PA, editors, FME 2002: Formal Methods - Getting IT Right: International Symposium of Formal Methods Europe Copenhagen, Denmark, July 22–24, 2002: Proceedings. Berlin, Heidelberg: Springer. 2002. p. 410-429. (Lecture Notes in Computer Science). https://doi.org/10.1007/3-540-45614-7_23