Interval change-point detection for runtime probabilistic model checking

Xingyu Zhao, Radu Calinescu, Simos Gerasimou, Valentin Robu, David Flynn

Research output: Chapter in Book/Report/Conference proceedingConference contribution

12 Citations (Scopus)
53 Downloads (Pure)


Recent probabilistic model checking techniques can verify reliability and performance properties of software systems affected by parametric uncertainty. This involves modelling the system behaviour using interval Markov chains, i.e., Markov models with transition probabilities or rates specified as intervals. These intervals can be updated continually using Bayesian estimators with imprecise priors, enabling the verification of the system properties of interest at runtime. However, Bayesian estimators are slow to react to sudden changes in the actual value of the estimated parameters, yielding inaccurate intervals and leading to poor verification results after such changes. To address this limitation, we introduce an efficient interval change-point detection method, and we integrate it with a state-of-the-art Bayesian estimator with imprecise priors. Our experimental results show that the resulting end-to-end Bayesian approach to change-point detection and estimation of interval Markov chain parameters handles effectively a wide range of sudden changes in parameter values, and supports runtime probabilistic model checking under parametric uncertainty.
Original languageEnglish
Title of host publicationASE '20: Proceedings of the 35th IEEE/ACM International Conference on Automated Software Engineering
PublisherAssociation for Computing Machinery
Number of pages12
ISBN (Print)9781450367684
Publication statusPublished - Dec 2020
Event35th IEEE/ACM International Conference on Automated Software Engineering 2020 - online, Melbourne, Australia
Duration: 21 Sept 202025 Sept 2020


Conference35th IEEE/ACM International Conference on Automated Software Engineering 2020
Abbreviated titleASE 2020


  • MCMC methods
  • Verification and validation
  • robot dynamics
  • change-point analysis
  • Runtime system
  • Formal methods
  • Bayes methods
  • interval Markov chains


Dive into the research topics of 'Interval change-point detection for runtime probabilistic model checking'. Together they form a unique fingerprint.

Cite this