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 – the middleware that supports it. 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.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Abrial, J.R.: The B-Book. Cambridge University Press, Cambridge (1996)
Abrial, J.R.: Modelling in Event-B. Cambridge University Press, Cambridge (2010)
Abrial, J.R., Cansell, D., Mery, D.: A mechanically proved and incremental development of IEEE 1394. Formal Aspects of Computing 14, 215–227 (2003)
Back, R., Sere, K.: Superposition refinement of reactive systems. Formal Aspects of Computing 8(3), 1–23 (1996)
Cansell, D., Méry, D.: Formal and incremental construction of distributed algorithms: on the distributed reference counting algorithm. Theoretical Computer Science 364, 318–337 (2006)
Degerlund, F., Walden, M., Sere, K.: Implementation issues concerning the action systems formalism. In: Proceedings of the Eighth International Conference on Parallel and Distributed Computing Applications and Technologies (PDCAT 2007). IEEE Computer Society, Los Alamitos (2007)
Dijkstra, E.: A Discipline of Programming. Prentice-Hall International, Englewood Cliffs (1976)
Fathabadi, S., Butler, M.: Applying Event-B Atomicity Decomposition to a Multi Media Protocol. In: de Boer, F.S., Bonsangue, M.M., Hallerstede, S., Leuschel, M. (eds.) FMCO 2009. LNCS, vol. 6286, pp. 89–104. Springer, Heidelberg (2010)
Garcia-Molina, H.: Elections in distributed computing systems. IEEE Transactions on Computers 31(1) (1982)
Hoang, T., Kuruma, H., Basin, D., Abrial, J.R.: Developing topology discovery in Event B. Science of Computer Programming 74 (2009)
Iliasov, A., Troubitsyna, E., Laibinis, L., Romanovsky, A., Varpaaniemi, K., Ilic, D., Latvala, T.: Supporting Reuse in Event B Development: Modularisation Approach. In: Frappier, M., Glässer, U., Khurshid, S., Laleau, R., Reeves, S. (eds.) ABZ 2010. LNCS, vol. 5977, pp. 174–188. Springer, Heidelberg (2010)
IST FP7 project DEPLOY, http://www.deploy-project.eu/
Butler, M., Yadav, D.: An incremental development of the Mondex system in Event B. Formal Aspects of Computing 20, 61–77 (2008)
Protocol, L.E.: Event B specification (2011), http://iliasov.org/modplugin/leaderel2commented.zip
Protocol, L.E.: Java implementation (2011), http://iliasov.org/modplugin/leaderel_program.zip
Rigorous Open Development Environment for Complex Systems (RODIN): Deliverable D7, Event B Language, http://rodin.cs.ncl.ac.uk/
RODIN modularisation plug-in: Documentation, http://wiki.event-b.org/index.php/Modularisation_Plug-in
The RODIN platform, http://rodin-b-sharp.sourceforge.net/
Walden, M.: Formal Reasoning About Distributed Algorithms. Åbo Akademi University, Finland, ph.D. Thesis (1998)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2011 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Iliasov, A., Laibinis, L., Troubitsyna, E., Romanovsky, A. (2011). Formal Derivation of a Distributed Program in Event B. In: Qin, S., Qiu, Z. (eds) Formal Methods and Software Engineering. ICFEM 2011. Lecture Notes in Computer Science, vol 6991. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-24559-6_29
Download citation
DOI: https://doi.org/10.1007/978-3-642-24559-6_29
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-24558-9
Online ISBN: 978-3-642-24559-6
eBook Packages: Computer ScienceComputer Science (R0)