Model exploration and analysis for quantitative safety refinement in probabilistic B

Details Model exploration and analysis for quantitative safety refinement in probabilistic B Model exploration and analysis for quantitative safety refinement in probabilistic B

2011-06-21

arxiv.org/abs/1106.4096v1

EPTCS 55, 2011, pp. 101-120

Computer Science

Logic in Computer Science

In Proceedings Refine 2011, arXiv:1106.3488

Scientific paper

10.4204/EPTCS.55.7

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.

Affiliated with

Also associated with

No associations

Rating

Model exploration and analysis for quantitative safety refinement in probabilistic B does not yet have a rating. At this time, there are no reviews or comments for this scientific paper.

If you have personal experience with Model exploration and analysis for quantitative safety refinement in probabilistic B, we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and Model exploration and analysis for quantitative safety refinement in probabilistic B will most certainly appreciate the feedback.

Rate now

Comments { 0 }

Profile ID: LFWR-SCP-O-177862