Abstract:


Qualitative Probabilistic Modelling in Event-B


Stefan Hallerstede and Thai Son Hoang



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 [18] 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.