Model exploration and analysis for quantitative safety refinement in probabilistic B

Ukachukwu Ndukwu, Annabelle McIver

Research output: Contribution to journalConference paperpeer-review


The role played by counterexamples in standard system analysis is well known; but less common is a notion of counterexample in probabilistic systems refinement. In this paper we extend previous work using counterexamples to inductive invariant properties of probabilistic systems, demonstrating how they can be used to extend the technique of bounded model checking-style analysis for the refinement of quantitative safety specifications in the probabilistic B language. In particular, we show how the method can be adapted to cope with refinements incorporating probabilistic loops. Finally, we demonstrate the technique on pB models summarising a one-step refinement of a randomised algorithm for finding the minimum cut of undirected graphs, and that for the dependability analysis of a controller design.
Original languageEnglish
Pages (from-to)101-120
Number of pages20
JournalProceedings of the 15th International Refinement Workshop (Refine 2011) : Limerick, Ireland, 20th June 2011
Publication statusPublished - 17 Jun 2011
EventInternational Refinement Workshop (15th : 2011) - Limerick, Ireland
Duration: 20 Jun 201120 Jun 2011


  • probabilistic B
  • quantitative safety specification
  • refinement
  • counterexamples


Dive into the research topics of 'Model exploration and analysis for quantitative safety refinement in probabilistic B'. Together they form a unique fingerprint.

Cite this