INCREMENTAL RUNTIME VERIFICATION OF PROBABLISTIC SYSTEMS
Probabilistic verification techniques have been proposed for runtime analysis of adaptive software systems, with the verification results being used to steer the system so that it satisfies certain Quality-of-Service requirements. Since systems evolve over time, and verification results are required...
| Main Authors: | , , , , |
|---|---|
| Format: | Report |
| Published: |
DCS
2012
|
| _version_ | 1797052764029714432 |
|---|---|
| author | Forejt, V Kwiatkowska, M Parker, D Qu, H Ujma, M |
| author_facet | Forejt, V Kwiatkowska, M Parker, D Qu, H Ujma, M |
| author_sort | Forejt, V |
| collection | OXFORD |
| description | Probabilistic verification techniques have been proposed for runtime analysis of adaptive software systems, with the verification results being used to steer the system so that it satisfies certain Quality-of-Service requirements. Since systems evolve over time, and verification results are required promptly, efficiency is an essential issue. To address this, we present incremental verification techniques, which exploit the results of previous analyses. We target systems modelled as Markov decision processes, developing incremental methods for constructing models from high-level system descriptions and for numerical solution using policy iteration based on strongly connected components. A prototype implementation, based on the PRISM model checker, demonstrates performance improvements on a range of case studies. |
| first_indexed | 2024-03-06T18:35:14Z |
| format | Report |
| id | oxford-uuid:0afc930c-5280-4a7d-991f-4148cccb8e68 |
| institution | University of Oxford |
| last_indexed | 2024-03-06T18:35:14Z |
| publishDate | 2012 |
| publisher | DCS |
| record_format | dspace |
| spelling | oxford-uuid:0afc930c-5280-4a7d-991f-4148cccb8e682022-03-26T09:27:03ZINCREMENTAL RUNTIME VERIFICATION OF PROBABLISTIC SYSTEMSReporthttp://purl.org/coar/resource_type/c_93fcuuid:0afc930c-5280-4a7d-991f-4148cccb8e68Department of Computer ScienceDCS2012Forejt, VKwiatkowska, MParker, DQu, HUjma, MProbabilistic verification techniques have been proposed for runtime analysis of adaptive software systems, with the verification results being used to steer the system so that it satisfies certain Quality-of-Service requirements. Since systems evolve over time, and verification results are required promptly, efficiency is an essential issue. To address this, we present incremental verification techniques, which exploit the results of previous analyses. We target systems modelled as Markov decision processes, developing incremental methods for constructing models from high-level system descriptions and for numerical solution using policy iteration based on strongly connected components. A prototype implementation, based on the PRISM model checker, demonstrates performance improvements on a range of case studies. |
| spellingShingle | Forejt, V Kwiatkowska, M Parker, D Qu, H Ujma, M INCREMENTAL RUNTIME VERIFICATION OF PROBABLISTIC SYSTEMS |
| title | INCREMENTAL RUNTIME VERIFICATION OF PROBABLISTIC SYSTEMS |
| title_full | INCREMENTAL RUNTIME VERIFICATION OF PROBABLISTIC SYSTEMS |
| title_fullStr | INCREMENTAL RUNTIME VERIFICATION OF PROBABLISTIC SYSTEMS |
| title_full_unstemmed | INCREMENTAL RUNTIME VERIFICATION OF PROBABLISTIC SYSTEMS |
| title_short | INCREMENTAL RUNTIME VERIFICATION OF PROBABLISTIC SYSTEMS |
| title_sort | incremental runtime verification of probablistic systems |
| work_keys_str_mv | AT forejtv incrementalruntimeverificationofprobablisticsystems AT kwiatkowskam incrementalruntimeverificationofprobablisticsystems AT parkerd incrementalruntimeverificationofprobablisticsystems AT quh incrementalruntimeverificationofprobablisticsystems AT ujmam incrementalruntimeverificationofprobablisticsystems |