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.
Type de document :
Communication dans un congrès
Shaz Qadeer. Runtime verification, Sep 2012, Istanbul, Turkey. Springer, 7687, pp.314-319, 2012, Lecture Notes in Computer Science
Liste complète des métadonnées

Littérature citée [8 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-00739483
Contributeur : Hongyang Qu <>
Soumis le : mercredi 10 octobre 2012 - 20:07:27
Dernière modification le : jeudi 11 octobre 2012 - 16:20:00
Document(s) archivé(s) le : vendredi 16 décembre 2016 - 21:41:02

Fichier

rv12.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : hal-00739483, version 1

Collections

Citation

Vojtech Forejt, Marta Kwiatkowska, David Parker, Hongyang Qu, Mateusz Ujma. Incremental Runtime Verification of Probabilistic Systems. Shaz Qadeer. Runtime verification, Sep 2012, Istanbul, Turkey. Springer, 7687, pp.314-319, 2012, Lecture Notes in Computer Science. 〈hal-00739483〉

Partager

Métriques

Consultations de la notice

107

Téléchargements de fichiers

105