Quantitative safety

linking proof-based verification with model checking for probabilistic systems

Ukachukwu Ndukwu

Research output: Chapter in Book/Report/Conference proceedingConference proceeding contribution

2 Citations (Scopus)

Abstract

This paper presents a novel approach for augmenting proof-based verification with performance-style analysis of the kind employed in state-of-the-art model checking tools for probabilistic systems. Quantitative safety properties usually specified as probabilistic system invariants and modeled in proof-based environments are evaluated using bounded model checking techniques. Our specific contributions include the statement of a theorem that is central to model checking safety properties of proof-based systems, the establishment of a procedure; and its full implementation in a prototype system (YAGA) which readily transforms a probabilistic model specified in a proof-based environment to its equivalent verifiable PRISM model equipped with reward structures. The reward structures capture the exact interpretation of the probabilistic invariants and can reveal succinct information about the model during experimental investigations. Finally, we demonstrate the novelty of the technique on a probabilistic library case study.
Original languageEnglish
Title of host publicationEPTCS 13
Subtitle of host publicationProceedings of the First Workshop on Quantitative Formal Methods: Theory and Applications (QFM 2009)
EditorsSuzana Andova, Annabelle McIver, Pedro D'Argenio, Pieter Cuijpers, Jasen Markovski, Caroll Morgan, Manuel Núñez
Place of Publicationonline
PublisherEPTCS
Pages27-40
Number of pages14
DOIs
Publication statusPublished - 2009
Externally publishedYes
EventFirst Workshop on Quantitative Formal Methods: Theory and Applications (QFM 2009) - Eindhoven, The Netherlands
Duration: 3 Nov 20093 Nov 2009

Workshop

WorkshopFirst Workshop on Quantitative Formal Methods: Theory and Applications (QFM 2009)
CityEindhoven, The Netherlands
Period3/11/093/11/09

Fingerprint Dive into the research topics of 'Quantitative safety: linking proof-based verification with model checking for probabilistic systems'. Together they form a unique fingerprint.

  • Cite this

    Ndukwu, U. (2009). Quantitative safety: linking proof-based verification with model checking for probabilistic systems. In S. Andova, A. McIver, P. D'Argenio, P. Cuijpers, J. Markovski, C. Morgan, & M. Núñez (Eds.), EPTCS 13: Proceedings of the First Workshop on Quantitative Formal Methods: Theory and Applications (QFM 2009) (pp. 27-40). online: EPTCS. https://doi.org/10.4204/EPTCS.13.3