Introducing probabilistic reasoning within Event-B

Event-B is a proof-based formal method used for discrete systems modelling. Several works have previously focused on the extension of Event-B for the description of probabilistic systems. In this paper, we propose an extension of Event-B that allows designing fully probabilistic systems as well as systems containing both probabilistic and non-deterministic choices. Compared to existing approaches which only focus on probabilistic assignments, our approach allows expressing probabilistic choices in all places where non-deterministic choices originally appear in a standard Event-B model: in the choice between enabled events, event parameter values and in probabilistic assignments. Furthermore, we introduce novel and adapted proof obligations for the consistency of such systems and introduce two key aspects to incremental design: probabilisation of existing events and refinement through the addition of new probabilistic events. In particular, we provide proof obligations for the almost-certain convergence of a set of new events, which is a required property in order to prove standard refinement in this context. Finally, we propose a fully detailed case study, which we use throughout the paper to illustrate our new constructions.