Yilmaz, Emre and Hoang, Thai Son Development of Rabin's Choice Coordination Algorithm in Event-B. Technical Report. University of Düsseldorf, Dusseldorf, Germany.
![]() | PDF 356Kb |
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.
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