Incremental Runtime Verification of Probabilistic Systems

Warning

This publication doesn't include Faculty of Economics and Administration. It includes Faculty of Informatics. Official publication website can be found on muni.cz.
Authors

FOREJT Vojtěch KWIATKOWSKA Marta PARKER David QU Hongyang UJMA Mateusz

Year of publication 2013
Type Article in Proceedings
Conference Runtime Verification
MU Faculty or unit

Faculty of Informatics

Citation
Web http://qav.comlab.ox.ac.uk/papers/rv12.pdf
Doi http://dx.doi.org/10.1007/978-3-642-35632-2_30
Field Informatics
Keywords Runtime verification; scalability; stochastic systems
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.
Related projects:

You are running an old browser version. We recommend updating your browser to its latest version.