Enhancing Proofs of Local Computations through Formal Event-B Modularization

Due to the lack of knowledge of the global state and the non determinism in the execution of the processes, distributed algorithms are considered to be very complex to design and to prove. However, it becomes crucial to guarantee that these algorithms run as designed. Modularization mechanism in formal development provides a simple way to manage this complexity. In this paper, we rely on the modularization mechanism of the Event-B method and on local computations model to propose a reuse based approach for modelling classes of distributed algorithms. The proposed approach consists in developing a formal pattern defined as a set of proved logical entities called modules. These modules are developed separately and, when needed, can be incorporated and instantiated in a given system development. Such a mechanism can save efforts on modelling and proving the computation steps in distributed algorithms.