{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,17]],"date-time":"2025-10-17T13:56:00Z","timestamp":1760709360774},"reference-count":25,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2017,7,7]],"date-time":"2017-07-07T00:00:00Z","timestamp":1499385600000},"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":["Int J Softw Tools Technol Transfer"],"published-print":{"date-parts":[[2019,4]]},"DOI":"10.1007\/s10009-017-0463-4","type":"journal-article","created":{"date-parts":[[2017,7,7]],"date-time":"2017-07-07T13:02:16Z","timestamp":1499432536000},"page":"165-181","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":10,"title":["Formal modeling and analysis of ad hoc Zone Routing Protocol in Event-B"],"prefix":"10.1007","volume":"21","author":[{"given":"Chunyan","family":"Fu","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Kougen","family":"Zheng","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2017,7,7]]},"reference":[{"issue":"1","key":"463_CR1","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/S1570-8705(03)00043-X","volume":"2","author":"M Abolhasan","year":"2004","unstructured":"Abolhasan, M., Wysocki, T., Dutkiewicz, E.: A review of routing protocols for mobile ad hoc networks. Ad Hoc Netw. 2(1), 1\u201322 (2004)","journal-title":"Ad Hoc Netw."},{"key":"463_CR2","volume-title":"The B-Book: Assigning Programs to Meanings","author":"JR Abrial","year":"2005","unstructured":"Abrial, J.R.: The B-Book: Assigning Programs to Meanings. Cambridge University Press, Cambridge (2005)"},{"key":"463_CR3","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":"463_CR4","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. (STTT) 12(6), 447\u2013466 (2010)","journal-title":"Int. J. Softw. Tools Technol. Transf. (STTT)"},{"key":"463_CR5","doi-asserted-by":"publisher","first-page":"178","DOI":"10.1007\/978-3-642-30885-7_13","volume-title":"Abstract State Machines, Alloy, B, VDM, and Z","author":"JR Abrial","year":"2012","unstructured":"Abrial, J.R., Su, W., Zhu, H.: Formalizing hybrid systems with Event-B. In: Derrick, J., Fitzgerald, J., Gnesi, S., Khurshid, S., Leuschel, M., Reeves, S., Riccobene, E. (eds.) Abstract State Machines, Alloy, B, VDM, and Z, pp. 178\u2013193. Springer, Berlin Heidelberg (2012). doi:\n                    10.1007\/978-3-642-30885-7_13"},{"issue":"4","key":"463_CR6","doi-asserted-by":"publisher","first-page":"538","DOI":"10.1145\/581771.581775","volume":"49","author":"K Bhargavan","year":"2002","unstructured":"Bhargavan, K., Obradovic, D., Gunter, C.A.: Formal verification of standards for distance vector routing protocols. J. ACM 49(4), 538\u2013576 (2002). doi:\n                    10.1145\/581771.581775","journal-title":"J. ACM"},{"key":"463_CR7","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-11936-6_5","volume-title":"Automated Technology for Verification and Analysis, Lecture Notes in Computer Science","author":"T Bourke","year":"2014","unstructured":"Bourke, T., van Glabbeek, R., H\u00f6fner, P.: A mechanized proof of loop freedom of the (untimed) AODV routing protocol. In: Cassez, F., Raskin, J.F. (eds.) Automated Technology for Verification and Analysis, Lecture Notes in Computer Science. Springer, Berlin (2014). doi:\n                    10.1007\/978-3-319-11936-6_5"},{"key":"463_CR8","doi-asserted-by":"publisher","first-page":"157","DOI":"10.1007\/978-3-642-33170-1_12","volume-title":"Industrial Deployment of System Engineering Methods","author":"M Butler","year":"2013","unstructured":"Butler, M., Voisin, L., Muller, T.: Tooling. In: Romanovsky, A., Thomas, M. (eds.) Industrial Deployment of System Engineering Methods, pp. 157\u2013185. Springer, Berlin Heidelberg (2013). doi:\n                    10.1007\/978-3-642-33170-1_12"},{"issue":"3","key":"463_CR9","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)","journal-title":"Theor. Comput. Sci."},{"key":"463_CR10","unstructured":"Clausen, T., Dearlove, C., Jacquet, P.: The optimized link state routing protocol version 2. draft-ietf-manet-olsrv2-00, Work in progress (2006)"},{"key":"463_CR11","unstructured":"Haas, Z.J., Pearlman, M.R., Samar, P.: The bordercast resolution protocol (BRP) for ad hoc networks. draft-ietf-manet-zone-brp-02.txt, IETF Internet Draft (2002)"},{"key":"463_CR12","unstructured":"Haas, Z.J., Pearlman, M.R., Samar, P.: The interzone routing protocol (IERP) for ad hoc networks. draft-ietf-manet-zone-ierp-02.txt, IETF Internet Draft (2002)"},{"key":"463_CR13","unstructured":"Haas, Z.J., Pearlman, M.R., Samar, P.: The intrazone routing protocol (IARP) for ad hoc networks. draft-ietf-manet-zone-iarp-02.txt, IETF Internet Draft (2002)"},{"key":"463_CR14","unstructured":"Haas, Z.J., Pearlman, M.R., Samar, P.: The zone routing protocol (ZRP) for ad hoc networks. draft-ietf-manet-zone-zrp-04.txt, IETF Internet Draft (2002)"},{"key":"463_CR15","first-page":"1","volume-title":"IFM, LNCS","author":"T Hoang","year":"2009","unstructured":"Hoang, T., Kuruma, H., Basin, D., Abrial, J.R.: Developing topology discovery in Event-B. In: Leuschel, M., Wehrheim, H. (eds.) IFM, LNCS, pp. 1\u201319. Springer, Berlin Heidelberg (2009)"},{"key":"463_CR16","doi-asserted-by":"publisher","first-page":"153","DOI":"10.1007\/978-0-585-29603-6_5","volume-title":"Mobile Computing","author":"DB Johnson","year":"1996","unstructured":"Johnson, D.B., Maltz, D.A.: Dynamic source routing in ad hoc wireless networks. In: Imielinski, T., Korth, H. (eds.) Mobile Computing, pp. 153\u2013181. Kluwer Academic Publishers, Dordrecht (1996)"},{"issue":"2","key":"463_CR17","doi-asserted-by":"publisher","first-page":"185","DOI":"10.1007\/s10009-007-0063-9","volume":"10","author":"M Leuschel","year":"2008","unstructured":"Leuschel, M., Butler, M.: ProB: an automated analysis toolset for the B method. STTT 10(2), 185\u2013203 (2008)","journal-title":"STTT"},{"key":"463_CR18","volume-title":"Distributed Algorithms","author":"NA Lynch","year":"1996","unstructured":"Lynch, N.A.: Distributed Algorithms. Morgan Kaufmann, San Francisco (1996)"},{"key":"463_CR19","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, LNCS","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.) Stabilization, Safety, and Security of Distributed Systems, LNCS, vol. 6976, pp. 401\u2013415. Springer, Berlin Heidelberg (2011)"},{"key":"463_CR20","unstructured":"M\u00e9tayer, C., Voisin, L.: The Event-B mathematical language (2009). \n                    http:\/\/wiki.event-b.org\/index.php\/Event-B_Mathematical_Language"},{"key":"463_CR21","doi-asserted-by":"publisher","first-page":"234","DOI":"10.1145\/190809.190336","volume":"24","author":"CE Perkins","year":"1994","unstructured":"Perkins, C.E., Bhagwat, P.: Highly dynamic destination-sequenced distance-vector routing (DSDV) for mobile computers. ACM SIGCOMM Comput. Commun. Rev. 24, 234\u2013244 (1994)","journal-title":"ACM SIGCOMM Comput. Commun. Rev."},{"key":"463_CR22","doi-asserted-by":"crossref","unstructured":"Perkins, C.E., Royer, E.M.: Ad-hoc on-demand distance vector routing. In: Mobile Computing Systems and Applications, 1999. Proceedings. WMCSA\u201999. Second IEEE Workshop, pp. 90\u2013100. IEEE (1999)","DOI":"10.1109\/MCSA.1999.749281"},{"issue":"4","key":"463_CR23","doi-asserted-by":"publisher","first-page":"595","DOI":"10.1109\/TNET.2004.833153","volume":"12","author":"P Samar","year":"2004","unstructured":"Samar, P., Pearlman, M.R., Haas, Z.J.: Independent zone routing: an adaptive hybrid routing framework for ad hoc wireless networks. IEEE\/ACM Trans. Network. (TON) 12(4), 595\u2013608 (2004)","journal-title":"IEEE\/ACM Trans. Network. (TON)"},{"key":"463_CR24","doi-asserted-by":"crossref","unstructured":"Wibling, O., Parrow, J., Pears, A.: Automatized verification of ad hoc routing protocols. In: Formal Techniques for Networked and Distributed Systems, FORTE 2004, LNCS, vol. 3235, pp. 343\u2013358. Springer (2004)","DOI":"10.1007\/978-3-540-30232-2_22"},{"key":"463_CR25","doi-asserted-by":"publisher","first-page":"72","DOI":"10.1007\/11943952_7","volume-title":"Mobile Ad-hoc and Sensor Networks, Lecture Notes in Computer Science","author":"H Yang","year":"2006","unstructured":"Yang, H., Zhang, X., Wang, Y.: A correctness proof of the dsr protocol. In: Cao, J., Stojmenovic, I., Jia, X., Das, S. (eds.) Mobile Ad-hoc and Sensor Networks, Lecture Notes in Computer Science, pp. 72\u201383. Springer, Berlin Heidelberg (2006). doi:\n                    10.1007\/11943952_7"}],"container-title":["International Journal on Software Tools for Technology Transfer"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-017-0463-4.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10009-017-0463-4\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-017-0463-4.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,4,4]],"date-time":"2019-04-04T05:41:22Z","timestamp":1554356482000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10009-017-0463-4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,7,7]]},"references-count":25,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2019,4]]}},"alternative-id":["463"],"URL":"https:\/\/doi.org\/10.1007\/s10009-017-0463-4","relation":{},"ISSN":["1433-2779","1433-2787"],"issn-type":[{"value":"1433-2779","type":"print"},{"value":"1433-2787","type":"electronic"}],"subject":[],"published":{"date-parts":[[2017,7,7]]},"assertion":[{"value":"7 July 2017","order":1,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}