Quantitative Verification in Practice

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademic

3 Downloads (Pure)

Abstract

Soon after the birth of model checking, the first theoretical achievements have been reported on the automated verification of quanti- tative system aspects such as discrete probabilities and continuous time. These theories have been extended in various dimensions, such as con- tinuous probabilities, cost constraints, discounting, hybrid phenomena, and combinations thereof. Due to unremitting improvements of under- lying algorithms and data structures, together with the availability of more advanced computing engines, these techniques are nowadays appli- cable to realistic designs. Powerful software tools allow these techniques to be applied by non-specialists, and efforts have been made to embed these techniques into industrial system design processes. Quantitative verification has a broad application potential — successful applications in embedded system design, hardware, security, safety-critical software, schedulability analysis, and systems biology exemplify this. It is fair to say, that over the years this application area grows rapidly and there is no sign that this will not continue. This session reports on applying state-of-the-art quantitative verification techniques and tools to a variety of industrial case studies.
Original languageEnglish
Title of host publicationLeveraging Applications of Formal Methods, Verification, and Validation
Subtitle of host publication4th International Symposium on Leveraging Applications, ISoLA 2010, Heraklion, Crete, Greece, October 18-21, 2010, Proceedings, Part II
Place of PublicationBerlin
PublisherSpringer
Pages127-127
Number of pages1
ISBN (Electronic)978-3-642-16561-0
ISBN (Print)978-3-642-16560-3
DOIs
Publication statusPublished - 2010
Event4th International Symposium On Leveraging Applications of Formal Methods, Verification and Validation, ISoLA 2010 - Heraklion, Greece
Duration: 18 Oct 201021 Oct 2010
Conference number: 4
http://isola-conference.org/isola2010/

Publication series

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

Conference

Conference4th International Symposium On Leveraging Applications of Formal Methods, Verification and Validation, ISoLA 2010
Abbreviated titleISoLA 2010
CountryGreece
CityHeraklion
Period18/10/1021/10/10
Internet address

Fingerprint

Systems analysis
Model checking
Embedded systems
Data structures
Cables
Availability
Engines
Costs
Systems Biology
Hardware security

Keywords

  • IR-75340
  • EWI-19155
  • METIS-275802

Cite this

Haverkort, B. R. H. M., Katoen, J-P., & Larsen, K. G. (2010). Quantitative Verification in Practice. In Leveraging Applications of Formal Methods, Verification, and Validation: 4th International Symposium on Leveraging Applications, ISoLA 2010, Heraklion, Crete, Greece, October 18-21, 2010, Proceedings, Part II (pp. 127-127). (Lecture Notes in Computer Science; Vol. 6416). Berlin: Springer. https://doi.org/10.1007/978-3-642-16561-0_17
Haverkort, Boudewijn R.H.M. ; Katoen, Joost-Pieter ; Larsen, Kim G. / Quantitative Verification in Practice. Leveraging Applications of Formal Methods, Verification, and Validation: 4th International Symposium on Leveraging Applications, ISoLA 2010, Heraklion, Crete, Greece, October 18-21, 2010, Proceedings, Part II. Berlin : Springer, 2010. pp. 127-127 (Lecture Notes in Computer Science).
@inproceedings{3cb8b3f63db4478381b2b9fc4164dc52,
title = "Quantitative Verification in Practice",
abstract = "Soon after the birth of model checking, the first theoretical achievements have been reported on the automated verification of quanti- tative system aspects such as discrete probabilities and continuous time. These theories have been extended in various dimensions, such as con- tinuous probabilities, cost constraints, discounting, hybrid phenomena, and combinations thereof. Due to unremitting improvements of under- lying algorithms and data structures, together with the availability of more advanced computing engines, these techniques are nowadays appli- cable to realistic designs. Powerful software tools allow these techniques to be applied by non-specialists, and efforts have been made to embed these techniques into industrial system design processes. Quantitative verification has a broad application potential — successful applications in embedded system design, hardware, security, safety-critical software, schedulability analysis, and systems biology exemplify this. It is fair to say, that over the years this application area grows rapidly and there is no sign that this will not continue. This session reports on applying state-of-the-art quantitative verification techniques and tools to a variety of industrial case studies.",
keywords = "IR-75340, EWI-19155, METIS-275802",
author = "Haverkort, {Boudewijn R.H.M.} and Joost-Pieter Katoen and Larsen, {Kim G.}",
note = "10.1007/978-3-642-16561-0",
year = "2010",
doi = "10.1007/978-3-642-16561-0_17",
language = "English",
isbn = "978-3-642-16560-3",
series = "Lecture Notes in Computer Science",
publisher = "Springer",
pages = "127--127",
booktitle = "Leveraging Applications of Formal Methods, Verification, and Validation",

}

Haverkort, BRHM, Katoen, J-P & Larsen, KG 2010, Quantitative Verification in Practice. in Leveraging Applications of Formal Methods, Verification, and Validation: 4th International Symposium on Leveraging Applications, ISoLA 2010, Heraklion, Crete, Greece, October 18-21, 2010, Proceedings, Part II. Lecture Notes in Computer Science, vol. 6416, Springer, Berlin, pp. 127-127, 4th International Symposium On Leveraging Applications of Formal Methods, Verification and Validation, ISoLA 2010, Heraklion, Greece, 18/10/10. https://doi.org/10.1007/978-3-642-16561-0_17

Quantitative Verification in Practice. / Haverkort, Boudewijn R.H.M.; Katoen, Joost-Pieter; Larsen, Kim G.

Leveraging Applications of Formal Methods, Verification, and Validation: 4th International Symposium on Leveraging Applications, ISoLA 2010, Heraklion, Crete, Greece, October 18-21, 2010, Proceedings, Part II. Berlin : Springer, 2010. p. 127-127 (Lecture Notes in Computer Science; Vol. 6416).

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademic

TY - GEN

T1 - Quantitative Verification in Practice

AU - Haverkort, Boudewijn R.H.M.

AU - Katoen, Joost-Pieter

AU - Larsen, Kim G.

N1 - 10.1007/978-3-642-16561-0

PY - 2010

Y1 - 2010

N2 - Soon after the birth of model checking, the first theoretical achievements have been reported on the automated verification of quanti- tative system aspects such as discrete probabilities and continuous time. These theories have been extended in various dimensions, such as con- tinuous probabilities, cost constraints, discounting, hybrid phenomena, and combinations thereof. Due to unremitting improvements of under- lying algorithms and data structures, together with the availability of more advanced computing engines, these techniques are nowadays appli- cable to realistic designs. Powerful software tools allow these techniques to be applied by non-specialists, and efforts have been made to embed these techniques into industrial system design processes. Quantitative verification has a broad application potential — successful applications in embedded system design, hardware, security, safety-critical software, schedulability analysis, and systems biology exemplify this. It is fair to say, that over the years this application area grows rapidly and there is no sign that this will not continue. This session reports on applying state-of-the-art quantitative verification techniques and tools to a variety of industrial case studies.

AB - Soon after the birth of model checking, the first theoretical achievements have been reported on the automated verification of quanti- tative system aspects such as discrete probabilities and continuous time. These theories have been extended in various dimensions, such as con- tinuous probabilities, cost constraints, discounting, hybrid phenomena, and combinations thereof. Due to unremitting improvements of under- lying algorithms and data structures, together with the availability of more advanced computing engines, these techniques are nowadays appli- cable to realistic designs. Powerful software tools allow these techniques to be applied by non-specialists, and efforts have been made to embed these techniques into industrial system design processes. Quantitative verification has a broad application potential — successful applications in embedded system design, hardware, security, safety-critical software, schedulability analysis, and systems biology exemplify this. It is fair to say, that over the years this application area grows rapidly and there is no sign that this will not continue. This session reports on applying state-of-the-art quantitative verification techniques and tools to a variety of industrial case studies.

KW - IR-75340

KW - EWI-19155

KW - METIS-275802

U2 - 10.1007/978-3-642-16561-0_17

DO - 10.1007/978-3-642-16561-0_17

M3 - Conference contribution

SN - 978-3-642-16560-3

T3 - Lecture Notes in Computer Science

SP - 127

EP - 127

BT - Leveraging Applications of Formal Methods, Verification, and Validation

PB - Springer

CY - Berlin

ER -

Haverkort BRHM, Katoen J-P, Larsen KG. Quantitative Verification in Practice. In Leveraging Applications of Formal Methods, Verification, and Validation: 4th International Symposium on Leveraging Applications, ISoLA 2010, Heraklion, Crete, Greece, October 18-21, 2010, Proceedings, Part II. Berlin: Springer. 2010. p. 127-127. (Lecture Notes in Computer Science). https://doi.org/10.1007/978-3-642-16561-0_17