{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,7]],"date-time":"2026-06-07T04:48:50Z","timestamp":1780807730509,"version":"3.54.1"},"reference-count":53,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2023,1,16]],"date-time":"2023-01-16T00:00:00Z","timestamp":1673827200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2023,1,16]],"date-time":"2023-01-16T00:00:00Z","timestamp":1673827200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Cluster Comput"],"published-print":{"date-parts":[[2023,4]]},"DOI":"10.1007\/s10586-022-03963-y","type":"journal-article","created":{"date-parts":[[2023,1,16]],"date-time":"2023-01-16T17:02:58Z","timestamp":1673888578000},"page":"1611-1629","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":6,"title":["Abstracting IoT protocols using timed process algebra and SPIN model checker"],"prefix":"10.1007","volume":"26","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-2211-5058","authenticated-orcid":false,"given":"N.","family":"Suresh Kumar","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"G.","family":"Santhosh Kumar","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2023,1,16]]},"reference":[{"issue":"2","key":"3963_CR1","doi-asserted-by":"publisher","first-page":"239","DOI":"10.1007\/s00165-014-0302-2","volume":"27","author":"P Zave","year":"2015","unstructured":"Zave, P.: A practical comparison of alloy and spin. Form. Asp. Computing 27(2), 239\u2013253 (2015)","journal-title":"Form. Asp. Computing"},{"key":"3963_CR2","doi-asserted-by":"crossref","unstructured":"Fatima, T., Saghar, K., Ihsan, A.: Evaluation of model checkers spin and uppaal for testing wireless sensor network routing protocols. In: 2015 12th International Bhurban Conference on Applied Sciences and Technology (IBCAST), pp. 263\u2013267 (2015). IEEE","DOI":"10.1109\/IBCAST.2015.7058514"},{"key":"3963_CR3","doi-asserted-by":"crossref","unstructured":"Sharma, O., Lewis, J., Miller, A., Dearle, A., Balasubramaniam, D., Morrison, R., Sventek, J.: Towards verifying correctness of wireless sensor network applications using insense and spin. In: International SPIN Workshop on Model Checking of Software, pp. 223\u2013240 (2009). Springer","DOI":"10.1007\/978-3-642-02652-2_19"},{"key":"3963_CR4","doi-asserted-by":"crossref","unstructured":"Fehnker, A., Gao, P.: Formal verification and simulation for performance analysis for probabilistic broadcast protocols. Ad-Hoc, Mobile, and Wireless Networks, p. 128 (2006)","DOI":"10.1007\/11814764_12"},{"issue":"SI","key":"3963_CR5","doi-asserted-by":"publisher","first-page":"75","DOI":"10.1145\/844128.844136","volume":"36","author":"M Musuvathi","year":"2002","unstructured":"Musuvathi, M., Park, D.Y., Chou, A., Engler, D.R., Dill, D.L.: Cmc: a pragmatic approach to model checking real code. ACM SIGOPS Operat. Syst. Rev. 36(SI), 75\u201388 (2002)","journal-title":"ACM SIGOPS Operat. Syst. Rev."},{"issue":"1","key":"3963_CR6","doi-asserted-by":"publisher","first-page":"497","DOI":"10.1007\/s10586-015-0518-9","volume":"19","author":"K-H Han","year":"2016","unstructured":"Han, K.-H., Bae, W.-S.: Proposing and verifying a security protocol for hash function-based iot communication system. Cluster Computing 19(1), 497\u2013504 (2016)","journal-title":"Cluster Computing"},{"issue":"4","key":"3963_CR7","first-page":"228","volume":"2","author":"MV Bharti","year":"2012","unstructured":"Bharti, M.V., Kumar, S.: Survey of network protocol verification techniques. Int. J. Sci. Res. Pub. 2(4), 228\u2013231 (2012)","journal-title":"Int. J. Sci. Res. Pub."},{"key":"3963_CR8","doi-asserted-by":"crossref","unstructured":"Bo\u0161na\u010dki, D., Dams, D.: Integrating real time into spin: a prototype implementation. In: Formal Description Techniques and Protocol Specification, Testing and Verification, pp. 423\u2013438. Springer, (1998)","DOI":"10.1007\/978-0-387-35394-4_26"},{"key":"3963_CR9","doi-asserted-by":"crossref","unstructured":"Tripakis, S., Courcoubetis, C.: Extending promela and spin for real time. In: International Workshop on Tools and Algorithms for the Construction and Analysis of Systems, pp. 329\u2013348 (1996). Springer","DOI":"10.1007\/3-540-61042-1_53"},{"key":"3963_CR10","doi-asserted-by":"crossref","unstructured":"Yacoub, A., Hamri, M.E.-A., Frydman, C.: Using dev-promela for modelling and verification of software. In: Proceedings of the 2016 ACM SIGSIM Conference on Principles of Advanced Discrete Simulation, pp. 245\u2013253 (2016)","DOI":"10.1145\/2901378.2901388"},{"issue":"1\u20134","key":"3963_CR11","first-page":"409","volume":"85","author":"W Nabia\u0142ek","year":"2008","unstructured":"Nabia\u0142ek, W., Janowska, A., Janowski, P.: Translation of timed promela to timed automata with discrete data. Fundam. Inform. 85(1\u20134), 409\u2013424 (2008)","journal-title":"Fundam. Inform."},{"key":"3963_CR12","doi-asserted-by":"crossref","unstructured":"C\u00e2mara, D., Loureiro, A.A.F., Filali, F.: Methodology for formal verification of routing protocols for ad hoc wireless networks. In: IEEE GLOBECOM 2007-IEEE Global Telecommunications Conference, pp. 705\u2013709 (2007). IEEE","DOI":"10.1109\/GLOCOM.2007.137"},{"issue":"1","key":"3963_CR13","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/0890-5401(92)90008-4","volume":"100","author":"R Milner","year":"1992","unstructured":"Milner, R., Parrow, J., Walker, D.: A calculus of mobile processes. Info. Computation 100(1), 1\u201340 (1992)","journal-title":"Info. Computation"},{"issue":"4","key":"3963_CR14","doi-asserted-by":"publisher","first-page":"511","DOI":"10.1093\/logcom\/2.4.511","volume":"2","author":"P Cousot","year":"1992","unstructured":"Cousot, P., Cousot, R.: Abstract interpretation frameworks. J. Logic Computation 2(4), 511\u2013547 (1992)","journal-title":"J. Logic Computation"},{"key":"3963_CR15","doi-asserted-by":"publisher","first-page":"24","DOI":"10.7146\/brics.v3i24.20005","volume":"3","author":"HE Jensen","year":"1996","unstructured":"Jensen, H.E., Larsen, K.G., Skou, A.: Modelling and analysis of a collision avoidance protocol using spin and uppaal. BRICS Rep. Series 3, 24 (1996)","journal-title":"BRICS Rep. Series"},{"key":"3963_CR16","doi-asserted-by":"crossref","unstructured":"Bodei, C., Degano, P., Nielson, F., Nielson, H.R.: Control flow analysis for the $$\\pi$$-calculus. In: International Conference on Concurrency Theory, pp. 84\u201398 (1998). Springer","DOI":"10.1007\/BFb0055617"},{"key":"3963_CR17","doi-asserted-by":"crossref","unstructured":"Venet, A.: Automatic determination of communication topologies in mobile systems. In: International Static Analysis Symposium, pp. 152\u2013167 (1998). Springer","DOI":"10.1007\/3-540-49727-7_9"},{"key":"3963_CR18","doi-asserted-by":"crossref","unstructured":"Bodei, C., Degano, P., Nielson, F., Nielson, H.R.: Static analysis of processes for no read-up and no write-down. In: International Conference on Foundations of Software Science and Computation Structure, pp. 120\u2013134 (1999). Springer","DOI":"10.1007\/3-540-49019-1_9"},{"key":"3963_CR19","doi-asserted-by":"crossref","unstructured":"Monniaux, D.: Abstracting crptographic protocols with tree automata. In: International Static Analysis Symposium, pp. 149\u2013163 (1999). Springer","DOI":"10.1007\/3-540-48294-6_10"},{"key":"3963_CR20","doi-asserted-by":"crossref","unstructured":"Feret, J.: Confidentiality analysis of mobile systems. In: International Static Analysis Symposium, pp. 135\u2013154 (2000). Springer","DOI":"10.1007\/978-3-540-45099-3_8"},{"issue":"2","key":"3963_CR21","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/S1571-0661(05)01155-2","volume":"39","author":"J Feret","year":"2000","unstructured":"Feret, J.: Occurrence counting analysis for the $$\\pi$$-calculus. Electron. Notes Theor. Computer Sci. 39(2), 1\u201318 (2000)","journal-title":"Electron. Notes Theor. Computer Sci."},{"key":"3963_CR22","doi-asserted-by":"crossref","unstructured":"Aziz, B., Hamilton, G.W.: A denotational semantics for the pi-calculus. In: IWFM (2001)","DOI":"10.14236\/ewic\/IWFM2001.3"},{"issue":"1","key":"3963_CR23","doi-asserted-by":"publisher","first-page":"68","DOI":"10.1006\/inco.2000.3020","volume":"168","author":"C Bodei","year":"2001","unstructured":"Bodei, C., Degano, P., Nielson, F., Nielson, H.R.: Static analysis for the $$\\pi$$-calculus with applications to security. Info. Computation 168(1), 68\u201392 (2001)","journal-title":"Info. Computation"},{"key":"3963_CR24","doi-asserted-by":"crossref","unstructured":"Feret, J.: Dependency analysis of mobile systems. In: European Symposium on Programming, pp. 314\u2013329 (2002). Springer","DOI":"10.1007\/3-540-45927-8_22"},{"key":"3963_CR25","unstructured":"Aziz, B.Y.: A static analysis framework for security properties in mobile and cryptographic systems. PhD thesis, Dublin City University (2003)"},{"issue":"1","key":"3963_CR26","doi-asserted-by":"publisher","first-page":"21","DOI":"10.1016\/S1571-0661(05)82502-2","volume":"39","author":"M Berger","year":"2003","unstructured":"Berger, M., Honda, K.: The two-phase commitment protocol in an extended $$\\pi$$-calculus. Electron. Notes Theor. Computer Sci. 39(1), 21\u201346 (2003)","journal-title":"Electron. Notes Theor. Computer Sci."},{"key":"3963_CR27","unstructured":"Oleshchuk, V.A.: Ad-hoc sensor networks: modeling, specification and verification. In: Second IEEE International Workshop on Intelligent Data Acquisition and Advanced Computing Systems: Technology and Applications, 2003. Proceedings, pp. 76\u201379 (2003). IEEE"},{"key":"3963_CR28","doi-asserted-by":"crossref","unstructured":"De Renesse, F., Aghvami, A.: Formal verification of ad-hoc routing protocols using spin model checker. In: Proceedings of the 12th IEEE Mediterranean Electrotechnical Conference (IEEE Cat. No. 04CH37521), vol. 3, pp. 1177\u20131182 (2004). IEEE","DOI":"10.1109\/MELCON.2004.1348275"},{"key":"3963_CR29","doi-asserted-by":"crossref","unstructured":"Wibling, O., Parrow, J., Pears, A.: Automatized verification of ad hoc routing protocols. In: International Conference on Formal Techniques for Networked and Distributed Systems, pp. 343\u2013358 (2004). Springer","DOI":"10.1007\/978-3-540-30232-2_22"},{"key":"3963_CR30","first-page":"704","volume":"6","author":"B Kusy","year":"2006","unstructured":"Kusy, B., Abdelwahed, S.: Ftsp protocol verification using spin. ISIS 6, 704 (2006)","journal-title":"ISIS"},{"key":"3963_CR31","doi-asserted-by":"crossref","unstructured":"Fehnker, A., van Hoesel, L., Mader, A.H., Davis, J., Gibbons, J.: Modelling and verification of the lmac protocol for wireless sensor networks. Lecture Notes in Computer Science 4591(7), (2007)","DOI":"10.1007\/978-3-540-73210-5_14"},{"key":"3963_CR32","doi-asserted-by":"crossref","unstructured":"Saha, I., Roy, S.: A finite state analysis of time-triggered can (ttcan) protocol using spin. In: 2007 International Conference on Computing: Theory and Applications (ICCTA\u201907), pp. 77\u201381 (2007). IEEE","DOI":"10.1109\/ICCTA.2007.4"},{"key":"3963_CR33","doi-asserted-by":"crossref","unstructured":"Aziz, B., Hamilton, G.: Detecting man-in-the-middle attacks by precise timing. In: 2009 Third International Conference on Emerging Security Information, Systems and Technologies, pp. 81\u201386 (2009). IEEE","DOI":"10.1109\/SECURWARE.2009.20"},{"key":"3963_CR34","unstructured":"Ali, H.B., Karim, M.R., Ashraf, M., Powers, D.M.: Modeling and verification of extensible authentication protocol for transport layer security in wireless lan environment. In: 2010 2nd International Conference on Software Technology and Engineering, vol. 2, pp. 2\u201341 (2010). IEEE"},{"issue":"4","key":"3963_CR35","doi-asserted-by":"publisher","first-page":"343","DOI":"10.1016\/j.csi.2011.12.001","volume":"34","author":"X He","year":"2012","unstructured":"He, X., Kumar, R., Mu, L., Gj\u00f8s\u00e6ter, T., Li, F.Y.: Formal verification of a cooperative automatic repeat request mac protocol. Computer Stand. Interfaces 34(4), 343\u2013354 (2012)","journal-title":"Computer Stand. Interfaces"},{"issue":"1","key":"3963_CR36","doi-asserted-by":"publisher","first-page":"87","DOI":"10.1016\/j.tcs.2011.07.018","volume":"413","author":"F Heidarian","year":"2012","unstructured":"Heidarian, F., Schmaltz, J., Vaandrager, F.: Analysis of a clock synchronization protocol for wireless sensor networks. Theor. Computer Sci. 413(1), 87\u2013105 (2012)","journal-title":"Theor. Computer Sci."},{"issue":"1","key":"3963_CR37","doi-asserted-by":"publisher","first-page":"122","DOI":"10.1016\/j.eswa.2012.07.030","volume":"40","author":"M El-Menshawy","year":"2013","unstructured":"El-Menshawy, M., Bentahar, J., El Kholy, W., Dssouli, R.: Verifying conformance of multi-agent commitment-based protocols. Expert Syst. Appl. 40(1), 122\u2013138 (2013)","journal-title":"Expert Syst. Appl."},{"key":"3963_CR38","doi-asserted-by":"publisher","first-page":"49","DOI":"10.1016\/j.adhoc.2015.05.013","volume":"36","author":"B Aziz","year":"2016","unstructured":"Aziz, B.: A formal model and analysis of an iot protocol. Ad Hoc Netw. 36, 49\u201357 (2016)","journal-title":"Ad Hoc Netw."},{"key":"3963_CR39","doi-asserted-by":"publisher","first-page":"299","DOI":"10.1016\/j.procs.2016.07.214","volume":"93","author":"AJ Vattakunnel","year":"2016","unstructured":"Vattakunnel, A.J., Kumar, N.S., Kumar, G.S.: Modelling and verification of coap over routing layer using spin model checker. Procedia Computer Sci. 93, 299\u2013308 (2016)","journal-title":"Procedia Computer Sci."},{"key":"3963_CR40","doi-asserted-by":"crossref","unstructured":"Kumar, N.S., Kumar, G.S.: Modeling and verification of timed automaton based hybrid systems using spin model checker. In: 2016 IEEE Annual India Conference (INDICON), pp. 1\u20138 (2016). IEEE","DOI":"10.1109\/INDICON.2016.7839011"},{"key":"3963_CR41","doi-asserted-by":"crossref","unstructured":"Aziz, B.: Modelling and analysing an industry 4.0 communication protocol. IEEE Internet of Things Journal (2020)","DOI":"10.1109\/JIOT.2020.2999325"},{"issue":"2","key":"3963_CR42","first-page":"323","volume":"31","author":"KK Raju","year":"2020","unstructured":"Raju, K.K.: Design and verification of wm protocol for electronic commerce transactions. Int. J. Indus. Eng. 31(2), 323\u2013338 (2020)","journal-title":"Int. J. Indus. Eng."},{"key":"3963_CR43","doi-asserted-by":"publisher","first-page":"100352","DOI":"10.1016\/j.vehcom.2021.100352","volume":"30","author":"B Aziz","year":"2021","unstructured":"Aziz, B.: A process algebraic mutation framework with application to a vehicle charging protocol. Vehi. Commun. 30, 100352 (2021)","journal-title":"Vehi. Commun."},{"issue":"4","key":"3963_CR44","doi-asserted-by":"publisher","first-page":"2977","DOI":"10.1007\/s10586-021-03305-4","volume":"24","author":"I Ben Hafaiedh","year":"2021","unstructured":"Ben Hafaiedh, I., Ben Hamouda, R., Robbana, R.: A model-based approach for formal verification and performance analysis of dynamic load-balancing protocols in cloud environment. Cluster Computing 24(4), 2977\u20132994 (2021)","journal-title":"Cluster Computing"},{"key":"3963_CR45","doi-asserted-by":"publisher","DOI":"10.1007\/s10586-022-03753-6","author":"S Zroug","year":"2022","unstructured":"Zroug, S., Remadna, I., Kahloul, L., Terrissa, S.L., Benharzallah, S.: Towards performance evaluation prediction in wsns using artificial neural network multi-perceptron. Cluster Computing (2022). https:\/\/doi.org\/10.1007\/s10586-022-03753-6","journal-title":"Cluster Computing"},{"issue":"2","key":"3963_CR46","doi-asserted-by":"publisher","first-page":"97","DOI":"10.1016\/S0140-3664(96)01150-4","volume":"20","author":"GJ Holzmann","year":"1997","unstructured":"Holzmann, G.J.: Designing bug-free protocols with spin. Computer Commun. 20(2), 97\u2013105 (1997)","journal-title":"Computer Commun."},{"issue":"5","key":"3963_CR47","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1109\/32.588521","volume":"23","author":"GJ Holzmann","year":"1997","unstructured":"Holzmann, G.J.: The model checker spin. IEEE Trans. Softw. Eng. 23(5), 279\u2013295 (1997)","journal-title":"IEEE Trans. Softw. Eng."},{"key":"3963_CR48","volume-title":"Principles of the spin model checker","author":"M Ben-Ari","year":"2008","unstructured":"Ben-Ari, M.: Principles of the spin model checker. Springer, Cham (2008)"},{"issue":"1","key":"3963_CR49","doi-asserted-by":"publisher","first-page":"40","DOI":"10.1145\/1721933.1721950","volume":"1","author":"MM Ben-Ari","year":"2010","unstructured":"Ben-Ari, M.M.: A primer on model checking. ACM Inroads 1(1), 40\u201347 (2010)","journal-title":"ACM Inroads"},{"key":"3963_CR50","unstructured":"Sewell, P.: Applied $$\\pi$$\u2013a brief tutorial. Technical report, University of Cambridge, Computer Laboratory (2000)"},{"key":"3963_CR51","doi-asserted-by":"crossref","unstructured":"Armstrong, R.C., Punnoose, R.J., Wong, M.H., Mayo, J.R.: Survey of existing tools for formal verification. Sandia Report SAND 2014-20533 (2014)","DOI":"10.2172\/1166644"},{"key":"3963_CR52","volume-title":"Lieberman: design and validation of computer protocols","author":"GJ Holzmann","year":"1991","unstructured":"Holzmann, G.J.: Lieberman: design and validation of computer protocols, vol. 512. Prentice Hall, Englewood Cliffs (1991)"},{"key":"3963_CR53","doi-asserted-by":"crossref","unstructured":"Levis, P., Clausen, T., Hui, J., Gnawali, O., Ko, J.: The trickle algorithm. Internet Engineering Task Force, RFC6206 (2011)","DOI":"10.17487\/rfc6206"}],"container-title":["Cluster Computing"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10586-022-03963-y.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10586-022-03963-y\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10586-022-03963-y.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,3,27]],"date-time":"2023-03-27T01:34:15Z","timestamp":1679880855000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10586-022-03963-y"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,1,16]]},"references-count":53,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2023,4]]}},"alternative-id":["3963"],"URL":"https:\/\/doi.org\/10.1007\/s10586-022-03963-y","relation":{},"ISSN":["1386-7857","1573-7543"],"issn-type":[{"value":"1386-7857","type":"print"},{"value":"1573-7543","type":"electronic"}],"subject":[],"published":{"date-parts":[[2023,1,16]]},"assertion":[{"value":"23 June 2022","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"23 December 2022","order":2,"name":"revised","label":"Revised","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"28 December 2022","order":3,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"16 January 2023","order":4,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}},{"order":1,"name":"Ethics","group":{"name":"EthicsHeading","label":"Declarations"}},{"value":"All authors declares that they have no conflict of interest to disclose.","order":2,"name":"Ethics","group":{"name":"EthicsHeading","label":"Conflict of interest"}},{"value":"This is the author\u2019s work not submitted anywhere else.","order":3,"name":"Ethics","group":{"name":"EthicsHeading","label":"Ethical approval"}},{"value":"NA.","order":4,"name":"Ethics","group":{"name":"EthicsHeading","label":"Informed consent"}}]}}