Abstract
The verification of distributed algorithms is a challenge for formal techniques supported by tools, such as model checkers and proof assistants. The difficulties lie in the derivation of proofs of required properties, such as safety and eventuality, for distributed algorithms. In this paper, we present a methodology based on the general concept of refinement that is used for developing distributed algorithms satisfying a given list of safety and liveness properties. The methodology is a recipe for reusing the old ingredients of the classical temporal approaches, which are illustrated through standard example of routing protocols. More precisely, we show how the state-based models can be developed for specific problems and how they can be simply reused by controlling the composition of state-based models through the refinement relationship. The service-as-event paradigm is introduced for helping users to describe algorithms as a composition of simple services and/or to decompose them into simple steps. Consequently, we obtain a framework to derive new distributed algorithms by developing existing distributed algorithms using correct-by-construction approach. The correct-by-construction approach ensures the correctness of developed distributed algorithms.
Access provided by Autonomous University of Puebla. Download to read the full chapter text
Chapter PDF
Similar content being viewed by others
Keywords
References
Abrial, J.-R.: Modeling in Event-B: System and Software Engineering (2010)
Abrial, J.-R., Cansell, D., Méry, D.: A mechanically proved and incremental development of ieee 1394 tree identify protocol. Formal Asp. Comput. 14(3), 215–227 (2003)
Abrial, J.-R., Hoang, T.S.: Using design patterns in formal methods: An event-B approach. In: Fitzgerald, J.S., Haxthausen, A.E., Yenigun, H. (eds.) ICTAC 2008. LNCS, vol. 5160, pp. 1–2. Springer, Heidelberg (2008)
Abrial, J.-R., Mussat, L.: Introducing Dynamic Constraints in B. In: B98, pp. 83–128 (1998)
Andriamiarina, M.B., Daoud, H., Belarbi, M., Méry, D., Tanougast, C.: Formal Verification of Fault Tolerant NoC-based Architecture. In: First International Workshop on Mathematics and Computer Science (IWMCS 2012), Tiaret, Algérie (December 2012)
Andriamiarina, M.B., Méry, D., Singh, N.K.: Revisiting Snapshot Algorithms by Refinement-based Techniques. In: PDCAT, IEEE Computer Society (2012)
Back, R.-J., Sere, K.: Stepwise refinement of action systems. Structured Programming 12(1), 17–30 (1991)
Cansell, D., Méry, D., Merz, S.: Diagram refinements for the design of reactive systems. J. UCS 7(2), 159–174 (2001)
Chandy, K.M., Misra, J.: Parallel Program Design A Foundation. Addison-Wesley Publishing Company (1988) ISBN 0-201-05866-9
Cisco Systems. Anycast RP, http://www.cisco.com/en/US/docs/ios/solutions_docs/ip_multicast/White_papers
Cisco Systems. Anycast RP using PIM, http://tools.ietf.org/html/draft-ietf-pim-anycast-rp-07
Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. MIT Press (2000)
Kang, J., Sucec, J., Kaul, V., Samtani, S., Fecko, M.A.: Robust pim-sm multicasting using anycast rp in wireless ad hoc networks. In: Proceedings of the 2009 IEEE International Conference on Communications, ICC 2009, pp. 5139–5144. IEEE Press, Piscataway (2009)
Lamport, L.: A temporal logic of actions. ACM Trans. Prog. Lang. Syst. 16(3), 872–923 (1994)
Leavens, G.T., Abrial, J.-R., Batory, D.S., Butler, M.J., Coglio, A., Fisler, K., Hehner, E.C.R., Jones, C.B., Miller, D., Jones, S.L.P., Sitaraman, M., Smith, D.R., Stump, A.: Roadmap for enhanced languages and methods to aid verification. In: Jarzabek, S., Schmidt, D.C., Veldhuizen, T.L. (eds.) GPCE, pp. 221–236. ACM (2006)
Manna, Z., Pnueli, A.: Temporal verification diagrams. In: Hagiya, M., Mitchell, J.C. (eds.) TACS 1994. LNCS, vol. 789, pp. 726–765. Springer, Heidelberg (1994)
McIver, A., Morgan, C.: Abstraction, Refinement And Proof For Probabilistic Systems (Monographs in Computer Science). Springer (2004)
Méry, D.: Requirements for a temporal B: Assigning Temporal Meaning to Abstract Machines. and to Abstract Systems. In: Galloway, A., Taguchi, K. (eds.) IFM 1999 Integrated Formal Methods 1999, YORK (June 1999)
Méry, D.: Refinement-based guidelines for algorithmic systems. Int. J. Software and Informatics 3(2-3), 197–239 (2009)
Méry, D., Singh, N.K.: Analysis of DSR protocol in event-B. In: Proceedings of the 13th International Conference on Stabilization, Safety, and Security of Distributed Systems, SSS 2011, pp. 401–415. Springer-Verlag, Heidelberg (2011)
Owicki, S., Gries, D.: An axiomatic proof technique for parallel programs I. Acta Informatica 6, 319–340 (1976)
Owicki, S., Lamport, L.: Proving liveness properties of concurrent programs. ACM Trans. Program. Lang. Syst. 4(3), 455–495 (1982)
Owre, S., Shankar, N.: A brief overview of PVS. In: Mohamed, O.A., Muñoz, C., Tahar, S. (eds.) TPHOLs 2008. LNCS, vol. 5170, pp. 22–27. Springer, Heidelberg (2008)
Project RODIN. Rigorous open development environment for complex systems (2004-2010), http://www.eventb.org/
Rehm, J., Cansell, D.: Proved Development of the Real-Time Properties of the IEEE 1394 Root Contention Protocol with the Event B Method. In: ISoLA, pp. 179–190 (2007)
Tanenbaum, A.S.: Computer networks (4. ed.). Prentice-Hall (2002)
Wenzel, M., Paulson, L.C., Nipkow, T.: The Isabelle Framework. In: Mohamed, O.A., Muñoz, C., Tahar, S. (eds.) TPHOLs 2008. LNCS, vol. 5170, pp. 33–38. Springer, Heidelberg (2008)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2013 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Andriamiarina, M.B., Méry, D., Singh, N.K. (2013). Integrating Proved State-Based Models for Constructing Correct Distributed Algorithms. In: Johnsen, E.B., Petre, L. (eds) Integrated Formal Methods. IFM 2013. Lecture Notes in Computer Science, vol 7940. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-38613-8_19
Download citation
DOI: https://doi.org/10.1007/978-3-642-38613-8_19
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-38612-1
Online ISBN: 978-3-642-38613-8
eBook Packages: Computer ScienceComputer Science (R0)