Moving from Event-B to probabilistic Event-B

Mohamed Amine Aouadhi (1) , Benoit Delahaye (2) , Arnaud Lanoix (1)

1 LINA - Laboratoire d'Informatique de Nantes Atlantique
2 AELOS

We propose a fully probabilistic extension of Event-B where all the non-deterministic choices are replaced with probabilities. We present the syntax and the semantics of this extension and introduce novel and adapted proof obligations for proving the correctness of probabilistic Event-B models. As a preliminary step towards handling refinement of probabilistic Event-B models, we propose sufficient conditions for the almost-certain convergence of a set of events and express them in terms of proof obligations. We illustrate our work by presenting a case study specified in both standard and probabilistic Event-B.

Mots clés: Event-B; Probabilities; Semantics; Almost-certain convergence

Domaines: Calcul formel [cs.SC]; Théorie et langage formel [cs.FL]

Mohamed Amine Aouadhi, Benoit Delahaye, Arnaud Lanoix. Moving from Event-B to probabilistic Event-B. [Research Report] LINA-University of Nantes. 2016. ⟨hal-01316610v2⟩