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. © Springer-Verlag Berlin Heidelberg 2007.
CITATION STYLE
Hallerstede, S., & Hoang, T. S. (2007). Qualitative probabilistic modelling in Event-B. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 4591 LNCS, pp. 293–312). Springer Verlag. https://doi.org/10.1007/978-3-540-73210-5_16
Mendeley helps you to discover research relevant for your work.