{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,14]],"date-time":"2026-04-14T03:58:25Z","timestamp":1776139105535,"version":"3.50.1"},"reference-count":51,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[2023,5,18]],"date-time":"2023-05-18T00:00:00Z","timestamp":1684368000000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2023,5,18]],"date-time":"2023-05-18T00:00:00Z","timestamp":1684368000000},"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":["SOCA"],"published-print":{"date-parts":[[2023,9]]},"DOI":"10.1007\/s11761-023-00363-x","type":"journal-article","created":{"date-parts":[[2023,5,18]],"date-time":"2023-05-18T21:02:04Z","timestamp":1684443724000},"page":"213-231","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":8,"title":["Formal modelling and verification of scalable service composition in IoT environment"],"prefix":"10.1007","volume":"17","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-4318-4415","authenticated-orcid":false,"given":"Sarah Hussein","family":"Toman","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Lazhar","family":"Hamel","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Zinah Hussein","family":"Toman","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Mohamed","family":"Graiet","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Samir","family":"Ouchani","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2023,5,18]]},"reference":[{"issue":"4","key":"363_CR1","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/s42979-021-00677-7","volume":"2","author":"T Alsboui","year":"2021","unstructured":"Alsboui T, Qin Y, Hill R, Al-Aqrabi H (2021) Distributed intelligence in the internet of things: challenges and opportunities. SN Comput Sci 2(4):1\u201316","journal-title":"SN Comput Sci"},{"issue":"3","key":"363_CR2","first-page":"291","volume":"30","author":"PP Ray","year":"2018","unstructured":"Ray PP (2018) A survey on internet of things architectures. J King Saud Univ Comput Inf Sci 30(3):291\u2013319","journal-title":"J King Saud Univ Comput Inf Sci"},{"key":"363_CR3","doi-asserted-by":"crossref","unstructured":"Spiess P, Karnouskos S, Guinard D, Savio D, Baecker O, De\u00a0Souza LMS, Trifa V (2009) Soa-based integration of the internet of things in enterprise services. In: 2009 IEEE international conference on web services. IEEE, pp 968\u2013975","DOI":"10.1109\/ICWS.2009.98"},{"key":"363_CR4","doi-asserted-by":"crossref","unstructured":"Lau K-K, Cola SD (2018) An introduction to component-based software developement. World Scientific","DOI":"10.1142\/10486"},{"key":"363_CR5","doi-asserted-by":"crossref","unstructured":"Paik H-Y, Lemos AL, Barukh MC, Benatallah B, Natarajan A (2017) Web service implementation and composition techniques. Springer","DOI":"10.1007\/978-3-319-55542-3"},{"key":"363_CR6","doi-asserted-by":"crossref","unstructured":"Arellanes D, Lau K-K (2018) Analysis and classification of service interactions for the scalability of the internet of things. In: 2018 IEEE international congress on internet of things (ICIOT). IEEE, pp\u00a080\u201387","DOI":"10.1109\/ICIOT.2018.00018"},{"key":"363_CR7","doi-asserted-by":"crossref","unstructured":"Yang Z, Li D (2014) Iot information service composition driven by user requirement. In: 2014 IEEE 17th international conference on computational science and engineering. IEEE, pp\u00a01509\u20131513","DOI":"10.1109\/CSE.2014.280"},{"issue":"5","key":"363_CR8","doi-asserted-by":"publisher","first-page":"3774","DOI":"10.1109\/JIOT.2018.2861742","volume":"5","author":"M Hamzei","year":"2018","unstructured":"Hamzei M, Navimipour NJ (2018) Toward efficient service composition techniques in the internet of things. IEEE Internet Things J 5(5):3774\u20133787","journal-title":"IEEE Internet Things J"},{"key":"363_CR9","doi-asserted-by":"crossref","unstructured":"Veal B, Foong A (2007) Performance scalability of a multi-core web server. In: Proceedings of the 3rd ACM\/IEEE symposium on architecture for networking and communications systems, pp\u00a057\u201366","DOI":"10.1145\/1323548.1323562"},{"issue":"5","key":"363_CR10","doi-asserted-by":"publisher","first-page":"686","DOI":"10.1109\/TKDE.2005.82","volume":"17","author":"Z Maamar","year":"2005","unstructured":"Maamar Z, Mostefaoui SK, Yahyaoui H (2005) Toward an agent-based and context-oriented approach for web services composition. IEEE Trans Knowl Data Eng 17(5):686\u2013697","journal-title":"IEEE Trans Knowl Data Eng"},{"key":"363_CR11","doi-asserted-by":"publisher","first-page":"827","DOI":"10.1016\/j.future.2020.02.073","volume":"108","author":"D Arellanes","year":"2020","unstructured":"Arellanes D, Lau K-K (2020) Evaluating iot service composition mechanisms for the scalability of iot systems. Futur Gener Comput Syst 108:827\u2013848","journal-title":"Futur Gener Comput Syst"},{"key":"363_CR12","unstructured":"Choe Y, Lee M (2018) Process model to predict nondeterministic behavior of iot systems. In: PrOse@ PoEM, pp\u00a01\u201312"},{"issue":"6","key":"363_CR13","doi-asserted-by":"publisher","first-page":"579","DOI":"10.1093\/comjnl\/35.6.579","volume":"35","author":"LM Barroca","year":"1992","unstructured":"Barroca LM, McDermid JA (1992) Formal methods: use and relevance for the development of safety-critical systems. Comput J 35(6):579\u2013599","journal-title":"Comput J"},{"key":"363_CR14","doi-asserted-by":"crossref","unstructured":"Abrial J-R (2018) On b and event-b: principles, success and challenges. In: International conference on abstract state machines, alloy, B, TLA, VDM, and Z. Springer, pp\u00a031\u201335","DOI":"10.1007\/978-3-319-91271-4_3"},{"issue":"6","key":"363_CR15","doi-asserted-by":"publisher","first-page":"447","DOI":"10.1007\/s10009-010-0145-y","volume":"12","author":"J-R Abrial","year":"2010","unstructured":"Abrial J-R, Butler M, Hallerstede S, Hoang TS, Mehta F, Voisin L (2010) Rodin: an open toolset for modelling and reasoning in event-b. Int J Softw Tools Technol Transfer 12(6):447\u2013466","journal-title":"Int J Softw Tools Technol Transfer"},{"issue":"1","key":"363_CR16","first-page":"41","volume":"5","author":"P Gokhale","year":"2018","unstructured":"Gokhale P, Bhat O, Bhat S (2018) Introduction to iot. Int Adv Res J Sci Eng Technol 5(1):41\u201344","journal-title":"Int Adv Res J Sci Eng Technol"},{"issue":"1","key":"363_CR17","first-page":"37","volume":"128","author":"ZH Ali","year":"2015","unstructured":"Ali ZH, Ali HA, Badawy MM (2015) Internet of things (iot): definitions, challenges and recent research directions. Int J Comput Appl 128(1):37\u201347","journal-title":"Int J Comput Appl"},{"key":"363_CR18","doi-asserted-by":"crossref","unstructured":"Bao F, Chen R, Guo J (2013) Scalable, adaptive and survivable trust management for community of interest based internet of things systems. In: 2013 IEEE eleventh international symposium on autonomous decentralized systems (ISADS). IEEE, pp\u00a01\u20137","DOI":"10.1109\/ISADS.2013.6513398"},{"key":"363_CR19","doi-asserted-by":"crossref","unstructured":"Chen J, Liu Y, Chai Y (2015) An identity management framework for internet of things. In: 2015 IEEE 12th international conference on e-business engineering. IEEE, pp\u00a0360\u2013364","DOI":"10.1109\/ICEBE.2015.67"},{"key":"363_CR20","doi-asserted-by":"crossref","unstructured":"Li K, Jiang L (2012) The research of web services composition based on context in internet of things. In: 2012 IEEE international conference on computer science and automation engineering (CSAE), vol\u00a01. IEEE, pp\u00a0160\u2013163","DOI":"10.1109\/CSAE.2012.6272570"},{"key":"363_CR21","doi-asserted-by":"crossref","unstructured":"Cabrera C, Li F, Nallur V, Palade A, Razzaque MA, White G, Clarke S (2017) Implementing heterogeneous, autonomous, and resilient services in iot: an experience report. In: 2017 IEEE 18th international symposium on a world of wireless, mobile and multimedia networks (WoWMoM). IEEE, pp\u00a01\u20136","DOI":"10.1109\/WoWMoM.2017.7974341"},{"key":"363_CR22","doi-asserted-by":"crossref","unstructured":"White G, Palade A, Clarke S (2018) Forecasting qos attributes using lstm networks. In: 2018 International joint conference on neural networks (IJCNN). IEEE, pp\u00a01\u20138","DOI":"10.1109\/IJCNN.2018.8489052"},{"key":"363_CR23","doi-asserted-by":"crossref","unstructured":"Ramparany F, Marquez FG, Soriano J, Elsaleh T (2014) Handling smart environment devices, data and services at the semantic level with the fi-ware core platform. In: 2014 IEEE international conference on big data (big data). IEEE, pp\u00a014\u201320","DOI":"10.1109\/BigData.2014.7004417"},{"key":"363_CR24","doi-asserted-by":"crossref","unstructured":"Wanigasekara N, Schmalfuss J, Carlson D, Rosenblum DS (2016) A bandit approach for intelligent iot service composition across heterogeneous smart spaces. In: Proceedings of the 6th international conference on the internet of things, pp\u00a0121\u2013129","DOI":"10.1145\/2991561.2991562"},{"issue":"11","key":"363_CR25","doi-asserted-by":"publisher","first-page":"2079","DOI":"10.1016\/j.jss.2008.04.044","volume":"81","author":"JM Ko","year":"2008","unstructured":"Ko JM, Kim CO, Kwon I-H (2008) Quality-of-service oriented web service composition algorithm and planning architecture. J Syst Softw 81(11):2079\u20132090","journal-title":"J Syst Softw"},{"issue":"1","key":"363_CR26","doi-asserted-by":"publisher","first-page":"15","DOI":"10.1109\/TSC.2008.1","volume":"1","author":"S-C Oh","year":"2008","unstructured":"Oh S-C, Lee D, Kumara SR (2008) Effective web service composition in diverse and large-scale service networks. IEEE Trans Serv Comput 1(1):15\u201332","journal-title":"IEEE Trans Serv Comput"},{"issue":"6","key":"363_CR27","doi-asserted-by":"publisher","first-page":"219","DOI":"10.1049\/iet-sen:20070027","volume":"1","author":"L Baresi","year":"2007","unstructured":"Baresi L, Bianculli D, Ghezzi C, Guinea S, Spoletini P (2007) Validation of web service compositions. IET Softw 1(6):219\u2013232","journal-title":"IET Softw"},{"key":"363_CR28","doi-asserted-by":"crossref","unstructured":"Sun H, Wang X, Zhou B, Zou P (2003) Research and implementation of dynamic web services composition. In: International workshop on advanced parallel processing technologies. Springer, pp\u00a0457\u2013466","DOI":"10.1007\/978-3-540-39425-9_54"},{"issue":"4","key":"363_CR29","doi-asserted-by":"publisher","first-page":"453","DOI":"10.1007\/s12652-015-0290-y","volume":"6","author":"Y Jararweh","year":"2015","unstructured":"Jararweh Y, Al-Ayyoub M, Darabseh A, Benkhelifa E, Vouk M, Rindos A (2015) Sdiot: a software defined based internet of things framework. J Ambient Intell Humaniz Comput 6(4):453\u2013461","journal-title":"J Ambient Intell Humaniz Comput"},{"key":"363_CR30","doi-asserted-by":"crossref","unstructured":"Bondi AB (2000) Characteristics of scalability and their impact on performance. In: Proceedings of the 2nd international workshop on software and performance, pp\u00a0195\u2013203","DOI":"10.1145\/350391.350432"},{"issue":"7","key":"363_CR31","first-page":"1617","volume":"13","author":"A Gupta","year":"2017","unstructured":"Gupta A, Christie R, Manjula R (2017) Scalability in internet of things: features, techniques and research challenges. Int J Comput Intell Res 13(7):1617\u20131627","journal-title":"Int J Comput Intell Res"},{"key":"363_CR32","doi-asserted-by":"crossref","unstructured":"Barzu A-P, Barbulescu M, Carabas M (2017) Horizontal scalability towards server performance improvement. In: 2017 16th RoEduNet conference: networking in education and research (RoEduNet). IEEE, pp\u00a01\u20136","DOI":"10.1109\/ROEDUNET.2017.8123729"},{"key":"363_CR33","doi-asserted-by":"publisher","first-page":"827","DOI":"10.1016\/j.future.2020.02.073","volume":"108","author":"D Arellanes","year":"2020","unstructured":"Arellanes D, Lau K-K (2020) Evaluating iot service composition mechanisms for the scalability of iot systems. Futur Gener Comput Syst 108:827\u2013848","journal-title":"Futur Gener Comput Syst"},{"key":"363_CR34","doi-asserted-by":"crossref","unstructured":"Arellanes D, Lau K-K (2019) Decentralized data flows in algebraic service compositions for the scalability of iot systems. In: 2019 IEEE 5th world forum on internet of things (WF-IoT). IEEE, pp\u00a0668\u2013673","DOI":"10.1109\/WF-IoT.2019.8767238"},{"key":"363_CR35","doi-asserted-by":"crossref","unstructured":"Arellanes D, Lau K-K (2018) Analysis and classification of service interactions for the scalability of the internet of things. In: 2018 IEEE international congress on internet of things (ICIOT). IEEE, pp\u00a080\u201387","DOI":"10.1109\/ICIOT.2018.00018"},{"key":"363_CR36","doi-asserted-by":"publisher","first-page":"253","DOI":"10.1016\/j.jss.2017.05.017","volume":"132","author":"R Khorsand","year":"2017","unstructured":"Khorsand R, Safi-Esfahani F, Nematbakhsh N, Mohsenzade M (2017) Taxonomy of workflow partitioning problems and methods in distributed environments. J Syst Softw 132:253\u2013271","journal-title":"J Syst Softw"},{"key":"363_CR37","doi-asserted-by":"crossref","unstructured":"Arellanes D, Lau K-K (2018) Algebraic service composition for user-centric iot applications. In: International conference on internet of things. Springer, pp\u00a056\u201369","DOI":"10.1007\/978-3-319-94370-1_5"},{"key":"363_CR38","doi-asserted-by":"crossref","unstructured":"Arellanes D, Lau K-K, Sakellariou R (2022) Decentralized data flows for the functional scalability of service-oriented iot systems. Comput J","DOI":"10.1093\/comjnl\/bxac023"},{"key":"363_CR39","doi-asserted-by":"crossref","unstructured":"Arellanes D, Lau K-K (2019) Decentralized data flows in algebraic service compositions for the scalability of iot systems. In: 2019 IEEE 5th world forum on internet of things (WF-IoT). IEEE, pp\u00a0668\u2013673","DOI":"10.1109\/WF-IoT.2019.8767238"},{"key":"363_CR40","doi-asserted-by":"crossref","unstructured":"Zhou W, Zhang Y, Wang J, Sun X, Chen Z, Yan X (2021) Ew2bpaas: a framework for effects web-based battle platform as a service. In: 2021 7th International conference on big data and information analytics (BigDIA). IEEE, pp\u00a0375\u2013384","DOI":"10.1109\/BigDIA53151.2021.9619724"},{"key":"363_CR41","doi-asserted-by":"publisher","first-page":"164","DOI":"10.1016\/j.scico.2014.04.015","volume":"94","author":"W Su","year":"2014","unstructured":"Su W, Abrial J-R, Zhu H (2014) Formalizing hybrid systems with event-b and the rodin platform. Sci Comput Program 94:164\u2013202","journal-title":"Sci Comput Program"},{"key":"363_CR42","doi-asserted-by":"crossref","unstructured":"Salehi\u00a0Fathabadi A, Rezazadeh A, Butler M (2011) Applying atomicity and model decomposition to a space craft system in event-b. In: NASA formal methods symposium. Springer, pp\u00a0328\u2013342","DOI":"10.1007\/978-3-642-20398-5_24"},{"key":"363_CR43","doi-asserted-by":"crossref","unstructured":"Tounsi I, Kacem MH, Kacem AH, Drira K (2015) A formal approach for soa design patterns composition. In: 2015 IEEE\/ACS 12th international conference of computer systems and applications (AICCSA). IEEE, pp\u00a01\u20138","DOI":"10.1109\/AICCSA.2015.7507154"},{"key":"363_CR44","doi-asserted-by":"crossref","unstructured":"Krishna A, Le\u00a0Pallec M, Mateescu R, Noirie L, Sala\u00fcn G (2019) Rigorous design and deployment of iot applications. In: 2019 IEEE\/ACM 7th international conference on formal methods in software engineering (FormaliSE). IEEE, pp\u00a011\u201320","DOI":"10.1109\/FormaliSE.2019.00011"},{"key":"363_CR45","unstructured":"Nadumane AKM (2020) Models and verification for composition and reconfiguration of web of things applications. PhD thesis, Universit\u00e9 Grenoble Alpes"},{"key":"363_CR46","unstructured":"Attiogb\u00e9 C, Rocheteau J (2019) Architectural invariants and correctness of iot-based systems. arXiv preprint arXiv:1912.08912"},{"key":"363_CR47","doi-asserted-by":"crossref","unstructured":"Lahouij A, Hamel L, Graiet M, El\u00a0Malki M (2018) A formal approach for cloud composite services verification. In: 2018 IEEE 11th conference on service-oriented computing and applications (SOCA). IEEE, pp\u00a0161\u2013168","DOI":"10.1109\/SOCA.2018.00031"},{"issue":"4","key":"363_CR48","doi-asserted-by":"publisher","first-page":"2453","DOI":"10.1007\/s10586-019-03018-9","volume":"23","author":"A Souri","year":"2020","unstructured":"Souri A, Rahmani AM, Navimipour NJ, Rezaei R (2020) A hybrid formal verification approach for qos-aware multi-cloud service composition. Clust Comput 23(4):2453\u20132470","journal-title":"Clust Comput"},{"key":"363_CR49","doi-asserted-by":"crossref","unstructured":"Tata S, Klai K, Jain R (2017) Formal model and method to decompose process-aware iot applications. In: OTM confederated international conferences \u201cOn the move to meaningful internet systems\u201d. Springer, pp\u00a0663\u2013680","DOI":"10.1007\/978-3-319-69462-7_42"},{"key":"363_CR50","doi-asserted-by":"crossref","unstructured":"Babin G, Ameur YA, Pantel M (2015) Formal verification of runtime compensation of web service compositions: a refinement and proof based proposal with event-b. In: 2015 IEEE international conference on services computing. IEEE, pp\u00a098\u2013105","DOI":"10.1109\/SCC.2015.23"},{"key":"363_CR51","doi-asserted-by":"crossref","unstructured":"Mahgoub A, Tarrad N, Elsherif R, Ismail L, Al-Ali A (2020) Fire alarm system for smart cities using edge computing. In: 2020 IEEE international conference on informatics, IoT, and enabling technologies (ICIoT). IEEE, pp\u00a0597\u2013602","DOI":"10.1109\/ICIoT48696.2020.9089653"}],"container-title":["Service Oriented Computing and Applications"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s11761-023-00363-x.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s11761-023-00363-x\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s11761-023-00363-x.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,7,22]],"date-time":"2023-07-22T10:09:18Z","timestamp":1690020558000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s11761-023-00363-x"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,5,18]]},"references-count":51,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2023,9]]}},"alternative-id":["363"],"URL":"https:\/\/doi.org\/10.1007\/s11761-023-00363-x","relation":{},"ISSN":["1863-2386","1863-2394"],"issn-type":[{"value":"1863-2386","type":"print"},{"value":"1863-2394","type":"electronic"}],"subject":[],"published":{"date-parts":[[2023,5,18]]},"assertion":[{"value":"6 July 2022","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"13 February 2023","order":2,"name":"revised","label":"Revised","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"10 April 2023","order":3,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"18 May 2023","order":4,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}