Abstract. The paper reports our investigation on tool support for the integration of qualitative probabilistic reasoning into Event-B. In the process, we formalise a non- trivial algorithm, namely Rabin’s choice coordination. Our correctness reasoning is a combination of termination proofs in terms of probabilistic convergence and standard invariant techniques. Moreover, we describe how qualitative probabilistic reasoning can be maintained during refinement.
Keywords: Event-B, qualitative reasoning, probabilistic termination, tool support, Rabin’s choice coordination.