Quantitative Safety: Linking Proof-Based Verification with Model Checking for Probabilistic Systems
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 pro...
| Main Author: | |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Open Publishing Association
2009-12-01
|
| Series: | Electronic Proceedings in Theoretical Computer Science |
| Online Access: | http://arxiv.org/pdf/0912.1900v1 |
| _version_ | 1828472364603539456 |
|---|---|
| author | Ukachukwu Ndukwu |
| author_facet | Ukachukwu Ndukwu |
| author_sort | Ukachukwu Ndukwu |
| collection | DOAJ |
| description | 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. |
| first_indexed | 2024-12-11T05:27:55Z |
| format | Article |
| id | doaj.art-8b7cd338a0c74b5e87fb0af7bbb5730d |
| institution | Directory Open Access Journal |
| issn | 2075-2180 |
| language | English |
| last_indexed | 2024-12-11T05:27:55Z |
| publishDate | 2009-12-01 |
| publisher | Open Publishing Association |
| record_format | Article |
| series | Electronic Proceedings in Theoretical Computer Science |
| spelling | doaj.art-8b7cd338a0c74b5e87fb0af7bbb5730d2022-12-22T01:19:31ZengOpen Publishing AssociationElectronic Proceedings in Theoretical Computer Science2075-21802009-12-0113Proc. QFM 2009273910.4204/EPTCS.13.3Quantitative Safety: Linking Proof-Based Verification with Model Checking for Probabilistic SystemsUkachukwu NdukwuThis 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.http://arxiv.org/pdf/0912.1900v1 |
| spellingShingle | Ukachukwu Ndukwu Quantitative Safety: Linking Proof-Based Verification with Model Checking for Probabilistic Systems Electronic Proceedings in Theoretical Computer Science |
| title | Quantitative Safety: Linking Proof-Based Verification with Model Checking for Probabilistic Systems |
| title_full | Quantitative Safety: Linking Proof-Based Verification with Model Checking for Probabilistic Systems |
| title_fullStr | Quantitative Safety: Linking Proof-Based Verification with Model Checking for Probabilistic Systems |
| title_full_unstemmed | Quantitative Safety: Linking Proof-Based Verification with Model Checking for Probabilistic Systems |
| title_short | Quantitative Safety: Linking Proof-Based Verification with Model Checking for Probabilistic Systems |
| title_sort | quantitative safety linking proof based verification with model checking for probabilistic systems |
| url | http://arxiv.org/pdf/0912.1900v1 |
| work_keys_str_mv | AT ukachukwundukwu quantitativesafetylinkingproofbasedverificationwithmodelcheckingforprobabilisticsystems |