Qualitative Probabilistic Modelling in Event-B

12 years 6 months ago
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.
Stefan Hallerstede, Thai Son Hoang
Added 08 Jun 2010
Updated 08 Jun 2010
Type Conference
Year 2007
Where IFM
Authors Stefan Hallerstede, Thai Son Hoang
Comments (0)