{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,12]],"date-time":"2025-11-12T14:27:26Z","timestamp":1762957646374,"version":"3.40.4"},"reference-count":54,"publisher":"Springer Science and Business Media LLC","issue":"4","license":[{"start":{"date-parts":[[2025,3,15]],"date-time":"2025-03-15T00:00:00Z","timestamp":1741996800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2025,3,15]],"date-time":"2025-03-15T00:00:00Z","timestamp":1741996800000},"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":["Computing"],"published-print":{"date-parts":[[2025,4]]},"DOI":"10.1007\/s00607-024-01358-y","type":"journal-article","created":{"date-parts":[[2025,3,15]],"date-time":"2025-03-15T02:14:08Z","timestamp":1742004848000},"update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["A formal approach for scalable applications in dynamic and constrained IoT-Cloud systems"],"prefix":"10.1007","volume":"107","author":[{"ORCID":"https:\/\/orcid.org\/0009-0006-7127-5222","authenticated-orcid":false,"given":"Yassmine","family":"Gara Hellal","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Lazhar","family":"Hamel","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Mohamed","family":"Graiet","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2025,3,15]]},"reference":[{"key":"1358_CR1","first-page":"77","volume":"9","author":"RARA Mouha","year":"2021","unstructured":"Mouha RARA et al (2021) Internet of Things (IoT). J Data Anal Inf Process 9:77","journal-title":"J Data Anal Inf Process"},{"issue":"3","key":"1358_CR2","first-page":"121","volume":"3","author":"UK Adyana","year":"2023","unstructured":"Adyana UK, Rai HP, Ogeti P, Fadnavis NS, Patil GB (2023) AI and machine learning in cloud-based internet of things (IoT) solutions: a comprehensive review and analysis. Int J Res Arts Human 3(3):121\u2013132","journal-title":"Int J Res Arts Human"},{"key":"1358_CR3","volume-title":"Service-oriented computing: 22nd international conference, ICSOC 2024, Tunis, Tunisia, December 3\u20136, 2024, Proceedings 22","author":"Y Gara Hellal","year":"2024","unstructured":"Gara Hellal Y, Hamel L, Graiet M (2024) An Event-B based approach for horizontally scalable IoT applications. In: Service-oriented computing: 22nd international conference, ICSOC 2024, Tunis, Tunisia, December 3\u20136, 2024, Proceedings 22. Springer"},{"key":"1358_CR4","doi-asserted-by":"crossref","unstructured":"He\u0111i I, \u0160peh I, \u0160arabok A (2017) IoT network protocols comparison for the purpose of IoT constrained networks. In: 2017 40th international convention on information and communication technology, electronics and microelectronics (MIPRO), pp. 501\u2013505. IEEE","DOI":"10.23919\/MIPRO.2017.7973477"},{"key":"1358_CR5","doi-asserted-by":"publisher","first-page":"347","DOI":"10.1109\/CCGrid59990.2024.00047","volume-title":"2024 IEEE 24th international symposium on cluster, cloud and internet computing (CCGrid)","author":"Y Gara Hellal","year":"2024","unstructured":"Gara Hellal Y, Hamel L, Graiet M, Balouek D (2024) A formal modeling and verification approach for IoT-Cloud resource-oriented applications. In: 2024 IEEE 24th international symposium on cluster, cloud and internet computing (CCGrid). IEEE, pp 347\u2013356"},{"issue":"1","key":"1358_CR6","doi-asserted-by":"publisher","first-page":"8","DOI":"10.3390\/jsan11010008","volume":"11","author":"I Rabet","year":"2022","unstructured":"Rabet I, Selvaraju SP, Fotouhi H, Alves M, Vahabi M, Balador A, Bj\u00f6rkman M (2022) Sdmob: Sdn-based mobility management for IoT networks. J Sens Actuator Netw 11(1):8","journal-title":"J Sens Actuator Netw"},{"issue":"1","key":"1358_CR7","first-page":"1","volume":"9","author":"Ahmed Mteaj","year":"2021","unstructured":"Mteaj A, Thakker U, Wang S, Li J, Amini MH (2021) A survey on federated learning for resource-constrained IoT devices. IEEE Internet Things J 9(1):1\u201324","journal-title":"IEEE Internet Things"},{"key":"1358_CR8","doi-asserted-by":"crossref","unstructured":"Shelby Z, Hartke K, Bormann C (2014) The constrained application protocol (CoAP)","DOI":"10.17487\/rfc7252"},{"key":"1358_CR9","doi-asserted-by":"publisher","first-page":"100829","DOI":"10.1016\/j.measen.2023.100829","volume":"28","author":"V Subrahmanyam","year":"2023","unstructured":"Subrahmanyam V, Kumar S, Srivastava S, Bist AS, Sah B, Pani NK, Bhambu P (2023) Optimizing horizontal scalability in Cloud computing using simulated annealing for internet of things. Meas Sens 28:100829","journal-title":"Meas Sens"},{"key":"1358_CR10","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. 57\u201366","DOI":"10.1145\/1323548.1323562"},{"key":"1358_CR11","doi-asserted-by":"publisher","first-page":"38","DOI":"10.1145\/1943371.1943378","volume":"36","author":"A Russo","year":"2011","unstructured":"Russo A (2011) Modeling in event-B: system and software engineering by jean-raymond abrial. ACM SIGSOFT Softw Eng Notes 36:38\u201339. https:\/\/doi.org\/10.1145\/1943371.1943378","journal-title":"ACM SIGSOFT Softw Eng Notes"},{"key":"1358_CR12","doi-asserted-by":"crossref","unstructured":"Abrial J-R (2018) On Bs and Event-B: principles, success and challenges. In: abstract state machines, Alloy, B, TLA, VDM, and Z: 6th international conference, ABZ 2018, Southampton, UK, June 5\u20138, 2018, Proceedings 6, pp. 31\u201335. Springer","DOI":"10.1007\/978-3-319-91271-4_3"},{"key":"1358_CR13","doi-asserted-by":"crossref","unstructured":"Bormann C, Ersue M, Keranen A (2014) Terminology for constrained-node networks","DOI":"10.17487\/rfc7228"},{"key":"1358_CR14","doi-asserted-by":"crossref","unstructured":"Irigon JI (2019) Adaptive routing for challenging networks. In: 2019 IEEE 4th international workshops on foundations and applications of self* systems (FAS* W), pp. 237\u2013239. IEEE","DOI":"10.1109\/FAS-W.2019.00062"},{"key":"1358_CR15","doi-asserted-by":"crossref","unstructured":"Kwanashie A, Obiniyi AA, Alkali JA, Ahmad BI (2023) Reviewing constrained node networks","DOI":"10.36227\/techrxiv.22015949.v2"},{"key":"1358_CR16","doi-asserted-by":"crossref","unstructured":"Rabet I, Fotouhi H, Alves M, Vahabi M, Bj\u00f6rkman M (2023) Actor: adaptive control of transmission power for routing in low-power and lossy networks","DOI":"10.36227\/techrxiv.24278218.v1"},{"key":"1358_CR17","unstructured":"Fielding RT (2000) Architectural styles and the design of network-based software architectures; doctoral dissertation"},{"key":"1358_CR18","doi-asserted-by":"publisher","first-page":"101491","DOI":"10.1016\/j.is.2020.101491","volume":"91","author":"N Niknejad","year":"2020","unstructured":"Niknejad N, Ismail W, Ghani I, Nazari B, Bahari M et al (2020) Understanding service-oriented architecture (soa): a systematic literature review and directions for further investigation. Inf Syst 91:101491","journal-title":"Inf Syst"},{"key":"1358_CR19","doi-asserted-by":"publisher","unstructured":"Shelby Z, Hartke K, Bormann C (2014) The constrained application protocol (CoAP). RFC Editor. https:\/\/doi.org\/10.17487\/RFC7252. https:\/\/www.rfc-editor.org\/info\/rfc7252","DOI":"10.17487\/RFC7252"},{"key":"1358_CR20","doi-asserted-by":"crossref","unstructured":"Bormann C, Ersue M, Keranen A (2014) RFC 7228: Terminology for constrained-node networks. RFC Editor","DOI":"10.17487\/rfc7228"},{"key":"1358_CR21","doi-asserted-by":"publisher","first-page":"9541","DOI":"10.1016\/j.jksuci.2021.11.007","volume":"34","author":"G Beniwal","year":"2022","unstructured":"Beniwal G, Singhrova A (2022) A systematic literature review on IoT gateways. J King Saud Univ Comput Inf Sci 34(10):9541\u20139563","journal-title":"J King Saud Univ Comput Inf Sci"},{"key":"1358_CR22","doi-asserted-by":"publisher","first-page":"947","DOI":"10.3390\/s23020947","volume":"23","author":"AK Tyagi","year":"2023","unstructured":"Tyagi AK, Dananjayan S, Agarwal D, Thariq Ahmed HF (2023) Blockchain-internet of things applications: opportunities and challenges for industry 4.0 and society 5.0. Sensors 23:947","journal-title":"Sensors"},{"issue":"5","key":"1358_CR23","first-page":"493","volume":"29","author":"A Abrar","year":"2023","unstructured":"Abrar A, Arif ASCM, Zaini KM (2023) Internet of things producer mobility management in named data networks: a survey, outlook, and open issues. Int J Commun Netw Distrib Syst 29(5):493\u2013512","journal-title":"Int J Commun Netw Distrib Syst"},{"key":"1358_CR24","doi-asserted-by":"publisher","first-page":"145","DOI":"10.1016\/j.future.2019.02.009","volume":"97","author":"MA Cruz","year":"2019","unstructured":"Cruz MA, Rodrigues JJ, Lorenz P, Solic P, Al-Muhtadi J, Albuquerque VHC (2019) A proposal for bridging application layer protocols to HTTP on IoT solutions. Future Gener Comput Syst 97:145\u2013152","journal-title":"Future Gener Comput Syst"},{"key":"1358_CR25","doi-asserted-by":"crossref","unstructured":"Azeez HH, Abdullah MZ (2023) Performance analysis of constrained application protocol (CoAP). In: AIP conference proceedings, vol. 2591. AIP Publishing","DOI":"10.1063\/5.0119584"},{"key":"1358_CR26","doi-asserted-by":"publisher","unstructured":"Patni S (2023) Fundamentals of RESTful APIs, pp. 1\u201315. https:\/\/doi.org\/10.1007\/978-1-4842-9200-6_1","DOI":"10.1007\/978-1-4842-9200-6_1"},{"key":"1358_CR27","doi-asserted-by":"crossref","unstructured":"Saviolo A, Loianno G (2023) Learning quadrotor dynamics for precise, safe, and agile flight control. Annual Reviews in Control","DOI":"10.1016\/j.arcontrol.2023.03.009"},{"key":"1358_CR28","doi-asserted-by":"publisher","unstructured":"Kizza J (2024) Internet of things (IoT): growth, challenges, and security, pp. 277\u2013291. https:\/\/doi.org\/10.1007\/978-3-319-70712-9_14","DOI":"10.1007\/978-3-319-70712-9_14"},{"key":"1358_CR29","doi-asserted-by":"publisher","first-page":"96322","DOI":"10.1109\/ACCESS.2022.3204042","volume":"10","author":"MA Razzaq","year":"2022","unstructured":"Razzaq MA, Mahar JA, Mehmood A, Choi GS, Ashraf I (2022) Simulation and assessment of vertical scaling for a smart campus environment using the internet of things. IEEE Access 10:96322\u201396330","journal-title":"IEEE Access"},{"issue":"7","key":"1358_CR30","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":"1358_CR31","doi-asserted-by":"crossref","unstructured":"Fahmi HZ, Lin FJ (2021) Nfv-enabled vertical scalability for IoT slices. In: 2021 22nd Asia-pacific network operations and management symposium (APNOMS), pp. 5\u20138. IEEE","DOI":"10.23919\/APNOMS52696.2021.9562612"},{"key":"1358_CR32","doi-asserted-by":"crossref","unstructured":"Singh M, Baranwal G (2018) Quality of service (qos) in internet of things. In: 2018 3rd international conference On internet of things: smart innovation and usages (IoT-SIU), pp. 1\u20136. IEEE","DOI":"10.1109\/IoT-SIU.2018.8519862"},{"key":"1358_CR33","doi-asserted-by":"crossref","unstructured":"Luntovskyy A, Globa L (2019) Performance, reliability and scalability for IoT. In: 2019 international conference on information and digital technologies (IDT), pp. 316\u2013321. IEEE","DOI":"10.1109\/DT.2019.8813679"},{"key":"1358_CR34","doi-asserted-by":"publisher","first-page":"102048","DOI":"10.1016\/j.inffus.2023.102048","volume":"102","author":"G Alwhishi","year":"2024","unstructured":"Alwhishi G, Bentahar J, Elwhishi A, Pedrycz W, Drawel N (2024) Multi-valued model 28 checking IoT and intelligent systems with commitment protocols in multi-source data environments. Inf Fusion 102:102048","journal-title":"Inf Fusion"},{"key":"1358_CR35","first-page":"184","volume-title":"The practice of enterprise modeling: 12th IFIP working conference, PoEM 2019, Luxembourg, Luxembourg, November 27\u201329, 2019, Proceedings 12","author":"S Junsup","year":"2019","unstructured":"Junsup S, Moonkun L (2019) Process algebra to control nondeterministic behavior of enterprise smart iot systems with probability. In: The practice of enterprise modeling: 12th IFIP working conference, PoEM 2019, Luxembourg, Luxembourg, November 27\u201329, 2019, Proceedings 12. Springer, pp 184\u2013196"},{"key":"1358_CR36","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 Trans 12:447\u2013466","journal-title":"Int J Softw Tools Technol Trans"},{"key":"1358_CR37","doi-asserted-by":"publisher","first-page":"100515","DOI":"10.1016\/j.iot.2022.100515","volume":"19","author":"F Dur\u00e1n","year":"2022","unstructured":"Dur\u00e1n F, Krishna A, Le Pallec M, Mateescu R, Sala\u00fcn G (2022) Models and analysis for user-driven reconfiguration of rule-based IoT applications. Internet Things 19:100515","journal-title":"Internet Things"},{"key":"1358_CR38","doi-asserted-by":"publisher","first-page":"767","DOI":"10.1109\/MODELS-C53483.2021.00123","volume-title":"2021 ACM\/IEEE international conference on model driven engineering languages and systems companion (MODELS-C)","author":"P Boutot","year":"2021","unstructured":"Boutot P, Tabassum MR, Mustafiz S (2021) UCM4IoT: a use case modelling environment for IoT systems. In: 2021 ACM\/IEEE international conference on model driven engineering languages and systems companion (MODELS-C). IEEE, pp 767\u2013776"},{"key":"1358_CR39","doi-asserted-by":"crossref","unstructured":"Reggio G (2018) A UML-based proposal for IoT system requirements specification. In: Proceedings of the 10th international workshop on modelling in software engineering, pp 9\u201316","DOI":"10.1145\/3193954.3193956"},{"key":"1358_CR40","first-page":"315","volume-title":"International conference on cybersecurity, cybercrimes, and smart emerging technologies","author":"A Paramonov","year":"2022","unstructured":"Paramonov A, Bushelenkov S, Tselykh A, Muthanna A, Koucheryavy A (2022) Model of the internet of things access network based on a lattice structure. In: International conference on cybersecurity, cybercrimes, and smart emerging technologies. Springer, pp 315\u2013322"},{"issue":"1","key":"1358_CR41","doi-asserted-by":"publisher","first-page":"47","DOI":"10.1007\/s12927-019-0003-8","volume":"11","author":"A Souri","year":"2019","unstructured":"Souri A, Norouzi M (2019) A state-of-the-art survey on formal verification of the internet of things applications. J Service Sci Res 11(1):47\u201367","journal-title":"J Service Sci Res"},{"key":"1358_CR42","doi-asserted-by":"crossref","unstructured":"Gara Hellal, Y., Hamel, L., Graiet, M.: Towards a Model for Energy-Efficient and Flexible IoT Systems. In: VECoS (2024).","DOI":"10.1007\/978-3-031-85356-2_13"},{"issue":"6","key":"1358_CR43","doi-asserted-by":"publisher","first-page":"3358","DOI":"10.1109\/TSC.2021.3094322","volume":"15","author":"D Kimovski","year":"2021","unstructured":"Kimovski D, Mehran N, Kerth CE, Prodan R (2021) Mobility-aware IoT application placement in the cloud-edge continuum. IEEE Trans Serv Comput 15(6):3358\u20133371","journal-title":"IEEE Trans Serv Comput"},{"key":"1358_CR44","doi-asserted-by":"crossref","unstructured":"Ray K, Banerjee A (2020) Trace-driven modeling and verification of a mobility-aware service allocation and migration policy for mobile edge computing. In: 2020 IEEE international conference on web services (ICWS), pp. 310\u2013317. IEEE","DOI":"10.1109\/ICWS49710.2020.00047"},{"key":"1358_CR45","doi-asserted-by":"publisher","unstructured":"Behera R, Patro A, Sinha\u00a0Roy D (2022) A resource-aware load balancing strategy for real-time, cross-vertical IoT applications, pp. 15\u201327. https:\/\/doi.org\/10.1007\/978-981-16-8739-6_2","DOI":"10.1007\/978-981-16-8739-6_2"},{"key":"1358_CR46","doi-asserted-by":"publisher","first-page":"43111","DOI":"10.1109\/ACCESS.2020.2976718","volume":"8","author":"J Hwang","year":"2020","unstructured":"Hwang J, Aziz A, Sung N, Ahmad A, Le Gall F, Song J (2020) Autocon-IoT: automated and scalable online conformance testing for IoT applications. IEEE Access 8:43111\u201343121","journal-title":"IEEE Access"},{"key":"1358_CR47","unstructured":"Tao X, Conzon D, Ferrera E, Li S, G\u00f6tz J, Maillet-Contoz L, Michel E, Diaz-Nava M, Baouya A, Chehida S (2020) Model based methodology and framework for design and management of next-gen IoT systems. In: SAM IoT, pp. 80\u201390"},{"key":"1358_CR48","doi-asserted-by":"crossref","unstructured":"Leotta M, Clerissi D, Franceschini L, Olianas D, Ancona D, Ricca F, Ribaudo M (2019) Comparing testing and runtime verification of IoT systems: a preliminary evaluation based on a case study. In: ENASE, pp. 434\u2013441","DOI":"10.5220\/0007745604340441"},{"key":"1358_CR49","doi-asserted-by":"crossref","unstructured":"Ouchani S (2018) Ensuring the functional correctness of IoT through formal modeling and verification. In: model and data engineering: 8th international conference, MEDI 2018, Marrakesh, Morocco, October 24\u201326, 2018, Proceedings 8, pp. 401\u2013417. Springer","DOI":"10.1007\/978-3-030-00856-7_27"},{"issue":"4","key":"1358_CR50","first-page":"739","volume":"7","author":"P Valsalan","year":"2020","unstructured":"Valsalan P, Baomar TAB, Baabood AHO (2020) Iot based health monitoring system. J Crit Rev 7(4):739\u2013743","journal-title":"J Crit Rev"},{"key":"1358_CR51","unstructured":"A formal approach for scalable applications in dynamic and constrained IoT systems. 2024. [online]. available: https:\/\/sites.google.com\/view\/formal-IoT-app"},{"key":"1358_CR52","doi-asserted-by":"publisher","first-page":"58032","DOI":"10.1109\/ACCESS.2020.2982472","volume":"8","author":"H Ramadhan","year":"2020","unstructured":"Ramadhan H, Indikawati FI, Kwon J, Koo B (2020) MusQ: a multi-store query system for IoT data using a datalog-like language. IEEE Access 8:58032\u201358056","journal-title":"IEEE Access"},{"key":"1358_CR53","unstructured":"Padidar S (2010) A study in the use of Event-B for system development from a software engineering viewpoint. Master\u2019s thesis, University of Edinburgh"},{"key":"1358_CR54","doi-asserted-by":"crossref","unstructured":"Leuschel M, Butler M (2003) Prob: A model checker for b. In: FME 2003: formal methods: international symposium of formal methods europe, Pisa, Italy, September 8-14, 2003. Proceedings, pp. 855\u2013874. Springer","DOI":"10.1007\/978-3-540-45236-2_46"}],"container-title":["Computing"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s00607-024-01358-y.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s00607-024-01358-y\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s00607-024-01358-y.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,4,26]],"date-time":"2025-04-26T17:52:08Z","timestamp":1745689928000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s00607-024-01358-y"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,3,15]]},"references-count":54,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2025,4]]}},"alternative-id":["1358"],"URL":"https:\/\/doi.org\/10.1007\/s00607-024-01358-y","relation":{},"ISSN":["0010-485X","1436-5057"],"issn-type":[{"type":"print","value":"0010-485X"},{"type":"electronic","value":"1436-5057"}],"subject":[],"published":{"date-parts":[[2025,3,15]]},"assertion":[{"value":"17 June 2024","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"31 October 2024","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"15 March 2025","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}},{"order":1,"name":"Ethics","group":{"name":"EthicsHeading","label":"Declarations"}},{"value":"The authors declare no competing interests.","order":2,"name":"Ethics","group":{"name":"EthicsHeading","label":"Conflict of interest"}}],"article-number":"96"}}