Abstract.We propose an approach for proving that a system guarantees to establish a given property eventually with probability one. Using Event-B as our modelling language, our correctness reasoning is a combination of termination proofs (in terms of probabilistic convergence), deadlock-freedom and invariant techniques. We illustrate the approach by formalising some non-trivial algorithms, including the duelling cowboys, Herman's probabilistic self-stabilization and Rabin's choice coordination. We extend the supporting Rodin Platform (Rodin) of Event-B to generate appropriate proof obligations for our reasoning, then subsequently (automatically/interactively) discharge the obligations using the built-in provers of Rodin.
Keywords: Event-B,formal modelling,probabilistic termination, almost-certain convergence, tool support, Herman's probabilistic self-stabilization, Rabin's choice coordination.