{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,27]],"date-time":"2025-10-27T16:07:22Z","timestamp":1761581242376},"reference-count":24,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[2014,10,23]],"date-time":"2014-10-23T00:00:00Z","timestamp":1414022400000},"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":["Telecommun Syst"],"published-print":{"date-parts":[[2015,3]]},"DOI":"10.1007\/s11235-014-9870-y","type":"journal-article","created":{"date-parts":[[2014,10,22]],"date-time":"2014-10-22T17:54:28Z","timestamp":1414000468000},"page":"205-217","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Modeling and analyzing the convergence property of the BGP routing protocol in SPIN"],"prefix":"10.1007","volume":"58","author":[{"given":"Zhe","family":"Chen","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Daqiang","family":"Zhang","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Yinxue","family":"Ma","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2014,10,23]]},"reference":[{"issue":"1\u20132","key":"9870_CR1","doi-asserted-by":"crossref","first-page":"61","DOI":"10.1007\/s11235-008-9088-y","volume":"38","author":"CJB Abbas","year":"2008","unstructured":"Abbas, C. J. B., Gonz\u00e1lez, R., Cardenas, N., & Garc\u00eda-Villalba, L. J. (2008). A proposal of a wireless sensor network routing protocol. Telecommunication Systems, 38(1\u20132), 61\u201368.","journal-title":"Telecommunication Systems"},{"key":"9870_CR2","volume-title":"Principles of model checking","author":"C Baier","year":"2008","unstructured":"Baier, C., & Katoen, J. P. (2008). Principles of model checking. Cambridge, MA: MIT Press."},{"key":"9870_CR3","volume-title":"Principles of the SPIN model checker","author":"M Ben-Ari","year":"2008","unstructured":"Ben-Ari, M. (2008). Principles of the SPIN model checker. Berlin: Springer."},{"issue":"2","key":"9870_CR4","doi-asserted-by":"crossref","first-page":"121","DOI":"10.1007\/s11235-009-9154-0","volume":"41","author":"YS Chen","year":"2009","unstructured":"Chen, Y. S., Liao, Y. J., Lin, Y. W., & Chiu, G. M. (2009). Hve-mobicast: A hierarchical-variant-egg-based mobicast routing protocol for wireless sensornets. Telecommunication Systems, 41(2), 121\u2013140.","journal-title":"Telecommunication Systems"},{"issue":"4","key":"9870_CR5","doi-asserted-by":"crossref","first-page":"299","DOI":"10.1007\/s11235-010-9294-2","volume":"46","author":"YS Chen","year":"2011","unstructured":"Chen, Y. S., Lin, Y. W., & Pan, C. Y. (2011). Dir: Diagonal-intersection-based routing protocol for vehicular ad hoc networks. Telecommunication Systems, 46(4), 299\u2013316.","journal-title":"Telecommunication Systems"},{"key":"9870_CR6","unstructured":"Chen, Z., Motet, G. (2010). Nevertrace claims for model checking. In Proceedings of the 17th International SPIN Workshop on Model Checking of Software (SPIN 2010), Lecture Notes in Computer Science, (vol. 6349, pp. 162\u2013179). Berlin: Springer."},{"key":"9870_CR7","volume-title":"Model Checking","author":"EM Clarke","year":"2000","unstructured":"Clarke, E. M., Grumberg, O., & Peled, D. A. (2000). Model Checking. Cambridge, MA: MIT Press."},{"issue":"2\/3","key":"9870_CR8","doi-asserted-by":"crossref","first-page":"275","DOI":"10.1007\/BF00121128","volume":"1","author":"C Courcoubetis","year":"1992","unstructured":"Courcoubetis, C., Vardi, M. Y., Wolper, P., & Yannakakis, M. (1992). Memory-efficient algorithms for the verification of temporal properties. Formal Methods in System Design, 1(2\/3), 275\u2013288.","journal-title":"Formal Methods in System Design"},{"key":"9870_CR9","unstructured":"Gastin, P., Oddoux, D. (2001). Fast LTL to B\u00fcchi automata translation. In Proceedings of the 13th International Conference on Computer Aided Verification (CAV\u201901), Lecture Notes in Computer Science, (vol. 2102, pp. 53\u201365). Berlin: Springer."},{"key":"9870_CR10","unstructured":"Gerth, R., Peled, D., Vardi, M. Y., & Wolper, P. (1995). Simple on-the-fly automatic verification of linear temporal logic. In P. Dembinski & M. Sredniawa (Eds.), Proceedings of the 15th IFIP WG6.1 International Symposium on Protocol Specification, Testing and Verification (pp. 3\u201318). London: Chapman & Hall."},{"issue":"2","key":"9870_CR11","doi-asserted-by":"crossref","first-page":"232","DOI":"10.1109\/90.993304","volume":"10","author":"T Griffin","year":"2002","unstructured":"Griffin, T., Shepherd, F. B., & Wilfong, G. T. (2002). The stable paths problem and interdomain routing. IEEE\/ACM Transactions on Networking (TON), 10(2), 232\u2013243.","journal-title":"IEEE\/ACM Transactions on Networking (TON)"},{"key":"9870_CR12","doi-asserted-by":"crossref","unstructured":"Griffin, T., & Wilfong, G.T. (1999). An analysis of bgp convergence properties. In Proceedings of the ACM SIGCOMM Conference on Applications, Technologies, Architectures, and Protocols for Computer Communication (SIGCOMM 1999), pp. 277\u2013288.","DOI":"10.1145\/316188.316231"},{"issue":"3\u20134","key":"9870_CR13","doi-asserted-by":"crossref","first-page":"291","DOI":"10.1023\/A:1016501430360","volume":"20","author":"P Herrmann","year":"2002","unstructured":"Herrmann, P., Krumm, H., Dr\u00f6gehorn, O., & Geisselhardt, W. (2002). Framework and tool support for formal verification of highspeed transfer protocol designs. Telecommunication Systems, 20(3\u20134), 291\u2013310.","journal-title":"Telecommunication Systems"},{"issue":"5","key":"9870_CR14","doi-asserted-by":"crossref","first-page":"279","DOI":"10.1109\/32.588521","volume":"23","author":"GJ Holzmann","year":"1997","unstructured":"Holzmann, G. J. (1997). The model checker SPIN. IEEE Transactions on Software Engineering, 23(5), 279\u2013295.","journal-title":"IEEE Transactions on Software Engineering"},{"issue":"3","key":"9870_CR15","doi-asserted-by":"crossref","first-page":"289","DOI":"10.1023\/A:1008696026254","volume":"13","author":"GJ Holzmann","year":"1998","unstructured":"Holzmann, G. J. (1998). An analysis of bitstate hashing. Formal Methods in System Design, 13(3), 289\u2013307.","journal-title":"Formal Methods in System Design"},{"key":"9870_CR16","volume-title":"The SPIN model checker: Primer and reference manual","author":"GJ Holzmann","year":"2003","unstructured":"Holzmann, G. J. (2003). The SPIN model checker: Primer and reference manual. Boston, MA: Addison-Wesley."},{"key":"9870_CR17","unstructured":"Huadmai, C. (2011). Verification of routing policies by using model checking technique. In Proceedings of the IEEE 6th International Conference on Intelligent Data Acquisition and Advanced Computing Systems: Technology and Applications (IDAACS 2011), (vol. 2, pp. 711\u2013716). IEEE."},{"key":"9870_CR18","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9780511810275","volume-title":"Logic in Computer science: Modelling and reasoning about systems","author":"M Huth","year":"2004","unstructured":"Huth, M., & Ryan, M. (2004). Logic in Computer science: Modelling and reasoning about systems (2nd ed.). Cambridge: Cambridge University Press.","edition":"2"},{"issue":"1\u20133","key":"9870_CR19","doi-asserted-by":"crossref","first-page":"255","DOI":"10.1007\/s11235-006-9014-0","volume":"33","author":"N Kettaf","year":"2006","unstructured":"Kettaf, N., Abouaissa, A., Duong, T. V., & Lorenz, P. (2006). An efficient QoS routing algorithm for solving MCP in ad hoc networks. Telecommunication Systems, 33(1\u20133), 255\u2013267.","journal-title":"Telecommunication Systems"},{"key":"9870_CR20","volume-title":"The art of software testing","author":"GJ Myers","year":"1979","unstructured":"Myers, G. J. (1979). The art of software testing. Hoboken, NJ: Wiley."},{"key":"9870_CR21","unstructured":"Rekhter, Y., & Li, T. (1995). A Border Gateway Protocol 4 (BGP-4), RFC 1771. IETF."},{"key":"9870_CR22","unstructured":"Rekhter, Y., & Li, T. (2006). A Border Gateway Protocol 4 (BGP-4), RFC 4271. IETF."},{"issue":"1\u20132","key":"9870_CR23","doi-asserted-by":"crossref","first-page":"77","DOI":"10.1007\/s11235-010-9335-x","volume":"48","author":"S Secci","year":"2011","unstructured":"Secci, S., Rougier, J. L., Pattavina, A., Patrone, F., & Maier, G. (2011). Multi-exit discriminator game for BGP routing coordination. Telecommunication Systems, 48(1\u20132), 77\u201392.","journal-title":"Telecommunication Systems"},{"key":"9870_CR24","unstructured":"Wang, A., Talcott, C. L., Jia, L., Loo, B. T., & Scedrov, A. (2011). Analyzing bgp instances in maude. In R. Bruni & J. Dingel (Eds.), Proceedings of the 31st IFIP WG 6.1 International Conference on Formal Techniques for Distributed Systems (FMOODS\/FORTE 2011), Lecture Notes in Computer Science (vol. 6722, pp. 334\u2013348). Berlin: Springer."}],"container-title":["Telecommunication Systems"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s11235-014-9870-y.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s11235-014-9870-y\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s11235-014-9870-y","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,6,1]],"date-time":"2019-06-01T06:50:17Z","timestamp":1559371817000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s11235-014-9870-y"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014,10,23]]},"references-count":24,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2015,3]]}},"alternative-id":["9870"],"URL":"https:\/\/doi.org\/10.1007\/s11235-014-9870-y","relation":{},"ISSN":["1018-4864","1572-9451"],"issn-type":[{"value":"1018-4864","type":"print"},{"value":"1572-9451","type":"electronic"}],"subject":[],"published":{"date-parts":[[2014,10,23]]}}}