Industrial deployment of system engineering methods providing high dependability and productivity


Development of Rabin's Choice Coordination Algorithm in Event-B

Yilmaz, Emre and Hoang, Thai Son Development of Rabin's Choice Coordination Algorithm in Event-B. Technical Report. University of Düsseldorf, Dusseldorf, Germany.



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.

Item Type:Monograph (Technical Report)
Subjects:Tool developments > Rodin plug-ins
Event-B > Event-B Examples
ID Code:258
Deposited By:Thai Son Hoang
Deposited On:01 Dec 2010 11:08
Last Modified:09 Dec 2010 15:37

Repository Staff Only: item control page

Deploy-Project - All right reserved