Model exploration and analysis for quantitative safety refinement in probabilistic B

Ukachukwu Ndukwu, Annabelle McIver

Research output: Contribution to journalConference paperResearchpeer-review

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.

Fingerprint

Model checking
Systems analysis
Specifications
Controllers

Cite this

@article{a4a582a1faaa4693b9914edd7d67f86d,
title = "Model exploration and analysis for quantitative safety refinement in probabilistic B",
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.",
keywords = "probabilistic B, quantitative safety specification, refinement, counterexamples",
author = "Ukachukwu Ndukwu and Annabelle McIver",
year = "2011",
month = "6",
day = "17",
doi = "10.4204/EPTCS.55.7",
language = "English",
volume = "55",
pages = "101--120",
journal = "Proceedings of the 15th International Refinement Workshop (Refine 2011) : Limerick, Ireland, 20th June 2011",
issn = "2075-2180",
publisher = "EPTCS",

}

Model exploration and analysis for quantitative safety refinement in probabilistic B. / Ndukwu, Ukachukwu; McIver, Annabelle.

In: Proceedings of the 15th International Refinement Workshop (Refine 2011) : Limerick, Ireland, 20th June 2011, Vol. 55, 17.06.2011, p. 101-120.

Research output: Contribution to journalConference paperResearchpeer-review

TY - JOUR

T1 - Model exploration and analysis for quantitative safety refinement in probabilistic B

AU - Ndukwu,Ukachukwu

AU - McIver,Annabelle

PY - 2011/6/17

Y1 - 2011/6/17

N2 - 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.

AB - 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.

KW - probabilistic B

KW - quantitative safety specification

KW - refinement

KW - counterexamples

UR - http://www.scopus.com/inward/record.url?scp=85022011321&partnerID=8YFLogxK

U2 - 10.4204/EPTCS.55.7

DO - 10.4204/EPTCS.55.7

M3 - Conference paper

VL - 55

SP - 101

EP - 120

JO - Proceedings of the 15th International Refinement Workshop (Refine 2011) : Limerick, Ireland, 20th June 2011

T2 - Proceedings of the 15th International Refinement Workshop (Refine 2011) : Limerick, Ireland, 20th June 2011

JF - Proceedings of the 15th International Refinement Workshop (Refine 2011) : Limerick, Ireland, 20th June 2011

SN - 2075-2180

ER -