Abstract : Abstract. We study distributed algorithms using the "correct-by-construction process", which involves the Event B method and the refinement process. These algorithms integrate non-functional requirements like probabilistic aspects. Therefore, it appears that the correct-by-construction process should integrate probabilistic arguments to be considered as a development and verification framework for distributed algorithms. We present here preliminary elements of a global approach on how to take into account probabilistic arguments during the development of distributed algorithms, and we illustrate this approach with the study of distributed coloring algorithms.
