title: Development of Rabin's Choice Coordination Algorithm in Event-B
creator: Yilmaz, Emre
creator: Hoang, Thai Son
subject: Rodin plug-ins
subject: Event-B Examples
description: The paper reports our investigation on tool support for the integration of qualitative probabilistic reasoning into Event-B.  In the process, we formalise a non-trivial algorithm, namely Rabin's choice coordination.  Our correctness reasoning is a combination of termination proofs in terms of probabilistic convergence and standard invariant techniques.  Moreover, we describe how qualitative probabilistic reasoning can be maintained during refinement.
publisher: University of Düsseldorf
type: Monograph
type: NonPeerReviewed
format: application/pdf
identifier: http://deploy-eprints.ecs.soton.ac.uk/258/1/rabin-llncs.pdf
identifier:   Yilmaz, Emre and Hoang, Thai Son   Development of Rabin's Choice Coordination Algorithm in Event-B.  Technical Report. University of Düsseldorf, Dusseldorf, Germany.     
relation: http://deploy-eprints.ecs.soton.ac.uk/258/