Skip to main content
Disciplines
Automotive Business IT + Informatics Construction + Real Estate Electrical Engineering + Electronics Energy + Sustainability Insurance + Risk Finance + Banking Management + Leadership Marketing + Sales Mechanical Engineering + Materials
Events
DE
EN
Books
Journals
Topic Page
Marketing
Start single access now
Access for companies
EXTENDED SEARCH
Log in
Top
Service Oriented Computing and Applications
Published in: Service Oriented Computing and Applications 3/2023

18-05-2023 | Original Research Paper

Formal modelling and verification of scalable service composition in IoT environment

Authors: Sarah Hussein Toman, Lazhar Hamel, Zinah Hussein Toman, Mohamed Graiet, Samir Ouchani

Published in: Service Oriented Computing and Applications | Issue 3/2023

Log in

Activate our intelligent search to find suitable subject content or patents.

search-config
loading …

Abstract

A system based on the internet of things (IoT) consists of services deployed across several devices that collaborate to fulfil IoT system goals. The growth in the number of IoT services that has occurred concurrently with the growth in the number of IoT devices is posing a significant difficulty for the process of service composition. In order to satisfy increasing demand and rapid expansion while keeping a certain level of quality of service, IoT systems need a scalable IoT service composition. However, building the correct scalable service composition is not guaranteed in IoT systems. This paper proposes formal modeling and verification of the scalability in IoT service composition at design time based on Event-B formal method. To fulfil the requirements of IoT service composition, the proposed model addresses more key qualities, mainly availability and interoperability. Further, by relying on the refinement technique, we create our model sequentially from the requirements analysis level to the target level. Finally, we validate and verify the correctness of the proposed formal model using of the Rodin platform and several proof obligations. Our verified model of the scalable IoT service composition has met its 44 proof obligations, and the Rodin prover was responsible for automatically addressing all of these proof obligations.
previous article SAKA: an intelligent platform for semi-automated knowledge graph construction and application

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

  • über 102.000 Bücher
  • über 537 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Maschinenbau + Werkstoffe
  • Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 390 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Maschinenbau + Werkstoffe




 

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 340 Zeitschriften

aus folgenden Fachgebieten:

  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Versicherung + Risiko




Jetzt Wissensvorsprung sichern!

inform now
Literature
1.
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–16CrossRef
2.
Ray PP (2018) A survey on internet of things architectures. J King Saud Univ Comput Inf Sci 30(3):291–319
3.
Spiess P, Karnouskos S, Guinard D, Savio D, Baecker O, De Souza 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–975
4.
Lau K-K, Cola SD (2018) An introduction to component-based software developement. World Scientific
5.
Paik H-Y, Lemos AL, Barukh MC, Benatallah B, Natarajan A (2017) Web service implementation and composition techniques. Springer
6.
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 80–87
7.
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 1509–1513
8.
Hamzei M, Navimipour NJ (2018) Toward efficient service composition techniques in the internet of things. IEEE Internet Things J 5(5):3774–3787CrossRef
9.
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–66
10.
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–697CrossRef
11.
Arellanes D, Lau K-K (2020) Evaluating iot service composition mechanisms for the scalability of iot systems. Futur Gener Comput Syst 108:827–848CrossRef
12.
Choe Y, Lee M (2018) Process model to predict nondeterministic behavior of iot systems. In: PrOse@ PoEM, pp 1–12
13.
Barroca LM, McDermid JA (1992) Formal methods: use and relevance for the development of safety-critical systems. Comput J 35(6):579–599CrossRef
14.
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 31–35
15.
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–466CrossRef
16.
Gokhale P, Bhat O, Bhat S (2018) Introduction to iot. Int Adv Res J Sci Eng Technol 5(1):41–44
17.
Ali ZH, Ali HA, Badawy MM (2015) Internet of things (iot): definitions, challenges and recent research directions. Int J Comput Appl 128(1):37–47
18.
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 1–7
19.
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 360–364
20.
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 1. IEEE, pp 160–163
21.
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 1–6
22.
White G, Palade A, Clarke S (2018) Forecasting qos attributes using lstm networks. In: 2018 International joint conference on neural networks (IJCNN). IEEE, pp 1–8
23.
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 14–20
24.
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 121–129
25.
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–2090CrossRef
26.
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–32CrossRef
27.
Baresi L, Bianculli D, Ghezzi C, Guinea S, Spoletini P (2007) Validation of web service compositions. IET Softw 1(6):219–232CrossRef
28.
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 457–466
29.
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–461CrossRef
30.
Bondi AB (2000) Characteristics of scalability and their impact on performance. In: Proceedings of the 2nd international workshop on software and performance, pp 195–203
31.
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–1627
32.
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 1–6
33.
Arellanes D, Lau K-K (2020) Evaluating iot service composition mechanisms for the scalability of iot systems. Futur Gener Comput Syst 108:827–848CrossRef
34.
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 668–673
35.
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 80–87
36.
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–271CrossRef
37.
Arellanes D, Lau K-K (2018) Algebraic service composition for user-centric iot applications. In: International conference on internet of things. Springer, pp 56–69
38.
Arellanes D, Lau K-K, Sakellariou R (2022) Decentralized data flows for the functional scalability of service-oriented iot systems. Comput J
39.
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 668–673
40.
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 375–384
41.
Su W, Abrial J-R, Zhu H (2014) Formalizing hybrid systems with event-b and the rodin platform. Sci Comput Program 94:164–202CrossRef
42.
Salehi Fathabadi 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 328–342
43.
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 1–8
44.
Krishna A, Le Pallec M, Mateescu R, Noirie L, Salaün 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 11–20
45.
Nadumane AKM (2020) Models and verification for composition and reconfiguration of web of things applications. PhD thesis, Université Grenoble Alpes
46.
47.
Lahouij A, Hamel L, Graiet M, El Malki M (2018) A formal approach for cloud composite services verification. In: 2018 IEEE 11th conference on service-oriented computing and applications (SOCA). IEEE, pp 161–168
48.
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–2470CrossRef
49.
Tata S, Klai K, Jain R (2017) Formal model and method to decompose process-aware iot applications. In: OTM confederated international conferences “On the move to meaningful internet systems”. Springer, pp 663–680
50.
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 98–105
51.
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 597–602
Metadata
Title
Formal modelling and verification of scalable service composition in IoT environment
Authors
Sarah Hussein Toman
Lazhar Hamel
Zinah Hussein Toman
Mohamed Graiet
Samir Ouchani
Publication date
18-05-2023
Publisher
Springer London
Published in
Service Oriented Computing and Applications / Issue 3/2023
Print ISSN: 1863-2386
Electronic ISSN: 1863-2394
DOI
https://doi.org/10.1007/s11761-023-00363-x

Other articles of this Issue 3/2023

Service Oriented Computing and Applications 3/2023 Go to the issue

Original Research Paper

SAKA: an intelligent platform for semi-automated knowledge graph construction and application

Editorial

Deep learning solutions for service-enabled systems and applications in Internet of Things

Original Research Paper

A SPARQL-based framework to preserve privacy of sensitive data on the semantic web

Original Research Paper

A configurable composition language for the social IoT

Original Research Paper

Qualitative and quantitative comparison of Spring Cloud and Kubernetes in migrating from a monolithic to a microservice architecture

Premium Partner

    Image Credits