creators_name: Yilmaz, Emre
creators_name: Hoang, Thai Son
creators_id: htson@inf.ethz.ch
type: monograph
datestamp: 2010-12-01 11:08:34
lastmod: 2010-12-09 15:37:25
metadata_visibility: show
title: Development of Rabin's Choice Coordination Algorithm in Event-B
ispublished: pub
subjects: deploy_tooldev_rodinplugins
subjects: examples
full_text_status: public
monograph_type: technical_report
abstract: 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
place_of_pub: Dusseldorf, Germany
institution: University of Düsseldorf
citation:   Yilmaz, Emre and Hoang, Thai Son   Development of Rabin's Choice Coordination Algorithm in Event-B.  Technical Report. University of Düsseldorf, Dusseldorf, Germany.     
document_url: http://deploy-eprints.ecs.soton.ac.uk/258/1/rabin-llncs.pdf