Qualitative Probabilistic Modelling in Event-B

Abstract. Event-B is a notation and method for discrete systems modelling by refinement. We introduce a small but very useful construction: qualitative probabilistic choice. It extends the expressiveness of Event-B allowing us to prove properties of systems that could not be formalised in Event-B before. We demonstrate this by means of a small example, part of a larger Event-B development that could not be fully proved before. An important feature of the introduced construction is that it does not complicate the existing Event-B notation or method, and can be explained without referring to the underlying more complicated probabilistic theory. The necessary theory [17] itself is briefly outlined in this article to justify the soundness of the proof obligations given. We also give a short account of alternative constructions that we explored, and rejected.

• Type: Conference
• Year: 2007
• Where: IFM
• Authors: Stefan Hallerstede, Thai Son Hoang
• Keywords: Complicated Probabilistic Theory, IFM 2007, Larger Event-b Development, Qualitative Probabilistic Choice