Skip to Main content Skip to Navigation
New interface
Conference papers

Incremental Runtime Verification of Probabilistic Systems

Abstract : Probabilistic veri cation techniques have been proposed for runtime analysis of adaptive software systems, with the veri cation results being used to steer the system so that it satis es certain Quality-of-Service requirements. Since systems evolve over time, and veri cation results are required promptly, e ciency is an essential issue. To address this, we present incremental veri cation 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.
Document type :
Conference papers
Complete list of metadata

Cited literature [8 references]  Display  Hide  Download
Contributor : Hongyang Qu Connect in order to contact the contributor
Submitted on : Wednesday, October 10, 2012 - 8:07:27 PM
Last modification on : Thursday, October 11, 2012 - 4:20:00 PM
Long-term archiving on: : Friday, December 16, 2016 - 9:41:02 PM


Files produced by the author(s)


  • HAL Id : hal-00739483, version 1



Vojtech Forejt, Marta Kwiatkowska, David Parker, Hongyang Qu, Mateusz Ujma. Incremental Runtime Verification of Probabilistic Systems. Runtime verification, Sep 2012, Istanbul, Turkey. pp.314-319. ⟨hal-00739483⟩



Record views


Files downloads