Model exploration and analysis for quantitative safety refinement in probabilistic B

TL;DR

This paper extends counterexample-based analysis techniques to probabilistic systems in the probabilistic B language, enabling refinement of quantitative safety properties including probabilistic loops, demonstrated on randomized algorithms and controller dependability models.

Contribution

It introduces a novel approach for using counterexamples in probabilistic system refinement, adapting bounded model checking for probabilistic loops in the probabilistic B framework.

Findings

Effective refinement of probabilistic safety specifications demonstrated

Counterexample-based analysis extended to probabilistic loops

Applied to randomized algorithms and controller models

Abstract

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.