creators_name: Iliasov, Alexei creators_name: Laibinis, Linas creators_name: Troubitsyna, Elena creators_name: Romanovsky, Alexander creators_id: "Alexei Iliasov" creators_id: Linas.Laibinis@abo.fi creators_id: Elena.Troubitsyna@abo.fi creators_id: alexander.romanovsky@ncl.ac.uk type: book_section datestamp: 2011-08-02 13:08:31 lastmod: 2011-08-02 13:11:37 metadata_visibility: show title: Formal Derivation of a Distributed Program in Event B ispublished: pub subjects: Event-Bsemantics subjects: Refinement subjects: deploy_method subjects: deploy_method_comp subjects: deploy_method_resil full_text_status: public abstract: Achieving high dependability of distributed systems remains a major challenge due to complexity arising from concurrency and communication. There are a number of formal approaches to verification of properties of distributed algorithms. However, there is still a lack of methods that enable a transition from a verified formal model of communication to a program that faithfully implements it. In this paper we aim at bridging this gap by proposing a state-based formal approach to correct-by-construction development of distributed programs. In our approach we take a systems view, i.e., formally model not only application but also its environment. We decompose such an integrated specification to obtain the distributed program that should be deployed on the targeted network infrastructure. To illustrate our approach, we present a development of a distributed leader election protocol. date: 2011 date_type: published publisher: Springer refereed: TRUE book_title: Proc of ICFEM 2011: 13th International Conference on Formal Engineering Methods. 26th—28th October 2011, Durham, United Kingdom citation: Iliasov, Alexei and Laibinis, Linas and Troubitsyna, Elena and Romanovsky, Alexander (2011) Formal Derivation of a Distributed Program in Event B. In: Proc of ICFEM 2011: 13th International Conference on Formal Engineering Methods. 26th—28th October 2011, Durham, United Kingdom. Springer. document_url: http://deploy-eprints.ecs.soton.ac.uk/320/1/paper_111.pdf