{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,26]],"date-time":"2025-03-26T07:04:46Z","timestamp":1742972686949,"version":"3.40.3"},"publisher-location":"Cham","reference-count":36,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030325046"},{"type":"electronic","value":"9783030325053"}],"license":[{"start":{"date-parts":[[2019,1,1]],"date-time":"2019-01-01T00:00:00Z","timestamp":1546300800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2019]]},"DOI":"10.1007\/978-3-030-32505-3_2","type":"book-chapter","created":{"date-parts":[[2019,10,25]],"date-time":"2019-10-25T22:09:57Z","timestamp":1572041397000},"page":"22-38","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["Verification by Construction of Distributed Algorithms"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-5231-6611","authenticated-orcid":false,"given":"Dominique","family":"M\u00e9ry","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2019,10,22]]},"reference":[{"key":"2_CR1","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9781139195881","volume-title":"Modeling in Event-B: System and Software Engineering","author":"JR Abrial","year":"2010","unstructured":"Abrial, J.R.: Modeling in Event-B: System and Software Engineering. Cambridge University Press, Cambridge (2010)"},{"issue":"6","key":"2_CR2","doi-asserted-by":"publisher","first-page":"447","DOI":"10.1007\/s10009-010-0145-y","volume":"12","author":"JR Abrial","year":"2010","unstructured":"Abrial, J.R., Butler, M., Hallerstede, S., Hoang, T.S., Mehta, F., Voisin, L.: Rodin: an open toolset for modelling and reasoning in Event-B. Int. J. Softw. Tools Technol. Transf. 12(6), 447\u2013466 (2010)","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"issue":"3","key":"2_CR3","doi-asserted-by":"publisher","first-page":"215","DOI":"10.1007\/s001650300002","volume":"14","author":"JR Abrial","year":"2003","unstructured":"Abrial, J.R., Cansell, D., M\u00e9ry, D.: A mechanically proved and incremental development of ieee 1394 tree identify protocol. Formal Asp. Comput. 14(3), 215\u2013227 (2003)","journal-title":"Formal Asp. Comput."},{"key":"2_CR4","doi-asserted-by":"publisher","first-page":"100","DOI":"10.1016\/j.scico.2015.12.004","volume":"121","author":"YA Ameur","year":"2016","unstructured":"Ameur, Y.A., M\u00e9ry, D.: Making explicit domain knowledge in formal system development. Sci. Comput. Program. 121, 100\u2013127 (2016). https:\/\/doi.org\/10.1016\/j.scico.2015.12.004","journal-title":"Sci. Comput. Program."},{"key":"2_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"117","DOI":"10.1007\/978-3-662-43652-3_9","volume-title":"Abstract State Machines, Alloy, B, TLA, VDM, and Z - 4th International Conference","author":"MB Andriamiarina","year":"2014","unstructured":"Andriamiarina, M.B., M\u00e9ry, D., Singh, N.K.: Analysis of self-$$\\star $$ and P2P systems using refinement. In: Ameur, Y.A., Schewe, K. (eds.) ABZ 2014. LNCS, vol. 8477, pp. 117\u2013123. Springer, USA (2014). https:\/\/doi.org\/10.1007\/978-3-662-43652-3_9"},{"issue":"1","key":"2_CR6","doi-asserted-by":"publisher","first-page":"251","DOI":"10.2298\/CSIS130122007A","volume":"11","author":"MB Andriamiarina","year":"2014","unstructured":"Andriamiarina, M.B., M\u00e9ry, D., Singh, N.K.: Revisiting snapshot algorithms by refinement-based techniques. Comput. Sci. Inf. Syst. 11(1), 251\u2013270 (2014). https:\/\/doi.org\/10.2298\/CSIS130122007A","journal-title":"Comput. Sci. Inf. Syst."},{"issue":"1","key":"2_CR7","first-page":"49","volume":"23","author":"R Back","year":"1979","unstructured":"Back, R.: On correct refinement of programs. Int. J. Softw. Tools Technol. Transf. 23(1), 49\u201368 (1979)","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"2_CR8","doi-asserted-by":"publisher","first-page":"593","DOI":"10.1007\/BF00291051","volume":"25","author":"R Back","year":"1998","unstructured":"Back, R.: A calculus of refinements for program derivations. Acta Informatica 25, 593\u2013624 (1998)","journal-title":"Acta Informatica"},{"key":"2_CR9","doi-asserted-by":"publisher","first-page":"1","DOI":"10.4204\/EPTCS.271.1","volume":"271","author":"Dines Bj\u00f8rner","year":"2018","unstructured":"Bj\u00f8rner, D.: Domain analysis & description - the implicit and explicit semantics problem. In: Laleau, R., M\u00e9ry, D., Nakajima, S., Troubitsyna, E. (eds.) Proceedings Joint Workshop on Handling IMPlicit and EXplicit Knowledge in Formal System Development (IMPEX) and Formal and Model-Driven Techniques for Developing Trustworthy Systems (FM&MDD), Xi\u2019An, China, 16th November 2017. Electronic Proceedings in Theoretical Computer Science, vol. 271, pp. 1\u201323. Open Publishing Association (2018). https:\/\/doi.org\/10.4204\/EPTCS.271.1","journal-title":"Electronic Proceedings in Theoretical Computer Science"},{"key":"2_CR10","doi-asserted-by":"publisher","unstructured":"Cansell, D., Gibson, J.P., M\u00e9ry, D.: Formal verification of tamper-evident storage for e-voting. In: Fifth IEEE International Conference on Software Engineering and Formal Methods (SEFM 2007), London, England, UK, 10\u201314 September 2007, pp. 329\u2013338. IEEE Computer Society (2007). https:\/\/doi.org\/10.1109\/SEFM.2007.21, https:\/\/doi.org\/10.1109\/SEFM.2007.21","DOI":"10.1109\/SEFM.2007.21 10.1109\/SEFM.2007.21"},{"issue":"3","key":"2_CR11","doi-asserted-by":"publisher","first-page":"318","DOI":"10.1016\/j.tcs.2006.08.015","volume":"364","author":"D Cansell","year":"2006","unstructured":"Cansell, D., M\u00e9ry, D.: Formal and incremental construction of distributed algorithms: on the distributed reference counting algorithm. Theor. Comput. Sci. 364(3), 318\u2013337 (2006). https:\/\/doi.org\/10.1016\/j.tcs.2006.08.015","journal-title":"Theor. Comput. Sci."},{"key":"2_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"17","DOI":"10.1007\/978-3-642-11447-2_2","volume-title":"Rigorous Methods for Software Construction and Analysis","author":"D Cansell","year":"2009","unstructured":"Cansell, D., M\u00e9ry, D.: Designing old and new distributed algorithms by replaying an incremental proof-based development. In: Abrial, J.-R., Gl\u00e4sser, U. (eds.) Rigorous Methods for Software Construction and Analysis. LNCS, vol. 5115, pp. 17\u201332. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-11447-2_2"},{"issue":"11","key":"2_CR13","doi-asserted-by":"publisher","first-page":"77","DOI":"10.1145\/384150.384165","volume":"44","author":"N Carriero","year":"2001","unstructured":"Carriero, N., Gelernter, D.: A computational model of everything. Commun. ACM 44(11), 77\u201381 (2001). https:\/\/doi.org\/10.1145\/384150.384165","journal-title":"Commun. ACM"},{"key":"2_CR14","unstructured":"Casteigts, A., Chaumette, S., Guinand, F., Pign\u00e9, Y.: Distributed maintenance of anytime available spanning trees in dynamic networks. CoRR abs\/0904.3087 (2009). http:\/\/arxiv.org\/abs\/0904.3087"},{"key":"2_CR15","unstructured":"Clearsy System Engineering: Atelier B (2002\u20132019). http:\/\/www.atelierb.eu\/"},{"key":"2_CR16","unstructured":"Clearsy System Engineering: BART (2010). http:\/\/tools.clearsy.com\/tools\/bart\/"},{"key":"2_CR17","doi-asserted-by":"publisher","DOI":"10.7551\/mitpress\/6156.001.0001","volume-title":"Self-Stabilization","author":"S Dolev","year":"2000","unstructured":"Dolev, S.: Self-Stabilization. MIT Press, Cambridge (2000)"},{"key":"2_CR18","doi-asserted-by":"crossref","unstructured":"Fakhfakh, F., Tounsi, M., Mosbah, M., M\u00e9ry, D., Kacem, A.H.: Proving distributed coloring of forests in dynamic networks. Computaci\u00f3n y Sistemas 21(4) (2017). http:\/\/www.cys.cic.ipn.mx\/ojs\/index.php\/CyS\/article\/view\/2857","DOI":"10.13053\/cys-21-4-2857"},{"key":"2_CR19","volume-title":"Designing and Building Parallel Programs - Concepts and Tools for Parallel Software Engineering","author":"IT Foster","year":"1995","unstructured":"Foster, I.T.: Designing and Building Parallel Programs - Concepts and Tools for Parallel Software Engineering. Addison-Wesley, Boston (1995)"},{"key":"2_CR20","volume-title":"Design Patterns: Elements of Reusable Object-Oriented Software Design Patterns","author":"E Gamma","year":"1994","unstructured":"Gamma, E., Helm, R., Johnson, R., Vlissides, R., Gamma, P.: Design Patterns: Elements of Reusable Object-Oriented Software Design Patterns. Addison-Wesley Professional Computing, Reading (1994)"},{"issue":"2","key":"2_CR21","doi-asserted-by":"publisher","first-page":"229","DOI":"10.1007\/s10270-010-0183-7","volume":"12","author":"TS Hoang","year":"2013","unstructured":"Hoang, T.S., F\u00fcrst, A., Abrial, J.: Event-B patterns and their tool support. Softw. Syst. Model. 12(2), 229\u2013244 (2013). https:\/\/doi.org\/10.1007\/s10270-010-0183-7","journal-title":"Softw. Syst. Model."},{"issue":"11\u201312","key":"2_CR22","doi-asserted-by":"publisher","first-page":"879","DOI":"10.1016\/j.scico.2009.07.006","volume":"74","author":"TS Hoang","year":"2009","unstructured":"Hoang, T.S., Kuruma, H., Basin, D.A., Abrial, J.: Developing topology discovery in Event-B. Sci. Comput. Program. 74(11\u201312), 879\u2013899 (2009). https:\/\/doi.org\/10.1016\/j.scico.2009.07.006","journal-title":"Sci. Comput. Program."},{"issue":"4","key":"2_CR23","doi-asserted-by":"publisher","first-page":"596","DOI":"10.1145\/69575.69577","volume":"5","author":"CB Jones","year":"1983","unstructured":"Jones, C.B.: Tentative steps toward a development method for interfering programs. ACM Trans. Program. Lang. Syst. 5(4), 596\u2013619 (1983). https:\/\/doi.org\/10.1145\/69575.69577","journal-title":"ACM Trans. Program. Lang. Syst."},{"issue":"3","key":"2_CR24","doi-asserted-by":"publisher","first-page":"872","DOI":"10.1145\/177492.177726","volume":"16","author":"L Lamport","year":"1994","unstructured":"Lamport, L.: The temporal logic of actions. ACM Trans. Program. Lang. Syst. 16(3), 872\u2013923 (1994)","journal-title":"ACM Trans. Program. Lang. Syst."},{"issue":"3","key":"2_CR25","doi-asserted-by":"publisher","first-page":"12:1","DOI":"10.1145\/2994595","volume":"39","author":"YA Liu","year":"2017","unstructured":"Liu, Y.A., Stoller, S.D., Lin, B.: From clarity to efficiency for distributed algorithms. ACM Trans. Program. Lang. Syst. 39(3), 12:1\u201312:41 (2017). https:\/\/doi.org\/10.1145\/2994595","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"2_CR26","series-title":"Springer Briefs in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4471-4201-0","volume-title":"Self-* and P2P for Network Management - Design Principles and Case Studies","author":"CC Marquezan","year":"2012","unstructured":"Marquezan, C.C., Granville, L.Z.: Self-* and P2P for Network Management - Design Principles and Case Studies. Springer Briefs in Computer Science. Springer, London (2012). https:\/\/doi.org\/10.1007\/978-1-4471-4201-0"},{"key":"2_CR27","unstructured":"M\u00e9ry, D.: Refinement-based guidelines for algorithmic systems. Int. J. Softw. Inform. 3(2\u20133), 197\u2013239 (2009). http:\/\/www.ijsi.org\/ch\/reader\/view_abstract.aspx?file_no=197&flag=1"},{"key":"2_CR28","doi-asserted-by":"publisher","first-page":"445","DOI":"10.1016\/j.future.2016.04.019","volume":"68","author":"D M\u00e9ry","year":"2017","unstructured":"M\u00e9ry, D.: Playing with state-based models for designing better algorithms. Future Gener. Comput. Syst. 68, 445\u2013455 (2017). https:\/\/doi.org\/10.1016\/j.future.2016.04.019","journal-title":"Future Gener. Comput. Syst."},{"key":"2_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"399","DOI":"10.1007\/978-3-030-03418-4_24","volume-title":"Leveraging Applications of Formal Methods, Verification and Validation. Modeling","author":"D M\u00e9ry","year":"2018","unstructured":"M\u00e9ry, D.: Modelling by patterns for correct-by-construction process. In: Margaria, T., Steffen, B. (eds.) ISoLA 2018. LNCS, vol. 11244, pp. 399\u2013423. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-030-03418-4_24"},{"key":"2_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"338","DOI":"10.1007\/978-3-642-21437-0_26","volume-title":"FM 2011: Formal Methods","author":"D M\u00e9ry","year":"2011","unstructured":"M\u00e9ry, D., Mosbah, M., Tounsi, M.: Refinement-based verification of local synchronization algorithms. In: Butler, M., Schulte, W. (eds.) FM 2011. LNCS, vol. 6664, pp. 338\u2013352. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-21437-0_26"},{"issue":"4","key":"2_CR31","doi-asserted-by":"publisher","first-page":"1083","DOI":"10.1007\/s10270-015-0504-y","volume":"16","author":"D M\u00e9ry","year":"2017","unstructured":"M\u00e9ry, D., Poppleton, M.: Towards an integrated formal method for verification of liveness properties in distributed systems: with application to population protocols. Softw. Syst. Model. 16(4), 1083\u20131115 (2017). https:\/\/doi.org\/10.1007\/s10270-015-0504-y","journal-title":"Softw. Syst. Model."},{"key":"2_CR32","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"401","DOI":"10.1007\/978-3-642-24550-3_30","volume-title":"Stabilization, Safety, and Security of Distributed Systems","author":"D M\u00e9ry","year":"2011","unstructured":"M\u00e9ry, D., Singh, N.K.: Analysis of DSR protocol in Event-B. In: D\u00e9fago, X., Petit, F., Villain, V. (eds.) SSS 2011. LNCS, vol. 6976, pp. 401\u2013415. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-24550-3_30"},{"key":"2_CR33","doi-asserted-by":"publisher","first-page":"319","DOI":"10.1007\/BF00268134","volume":"6","author":"S Owicki","year":"1976","unstructured":"Owicki, S., Gries, D.: An axiomatic proof technique for parallel programs I. Acta Informatica 6, 319\u2013340 (1976)","journal-title":"Acta Informatica"},{"key":"2_CR34","volume-title":"How to Solve It","author":"G Polya","year":"1957","unstructured":"Polya, G.: How to Solve It, 2nd edn. Princeton University Press, Princeton (1957). ISBN 0-691-08097-6","edition":"2"},{"key":"2_CR35","doi-asserted-by":"publisher","unstructured":"Tounsi, M., Mosbah, M., M\u00e9ry, D.: Proving distributed algorithms by combining refinement and local computations. ECEASST 35 (2010). https:\/\/doi.org\/10.14279\/tuj.eceasst.35.442","DOI":"10.14279\/tuj.eceasst.35.442"},{"key":"2_CR36","unstructured":"ViSiDiA (2006\u20132019). http:\/\/visidia.labri.fr"}],"container-title":["Lecture Notes in Computer Science","Theoretical Aspects of Computing \u2013 ICTAC 2019"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-32505-3_2","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,3,13]],"date-time":"2024-03-13T16:56:20Z","timestamp":1710348980000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-030-32505-3_2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019]]},"ISBN":["9783030325046","9783030325053"],"references-count":36,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-32505-3_2","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2019]]},"assertion":[{"value":"22 October 2019","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"ICTAC","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Colloquium on Theoretical Aspects of Computing","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Hammamet","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Tunisia","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2019","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"31 October 2019","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"4 November 2019","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"16","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"ictac2019","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/www.redcad.org\/events\/ictac2019\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}