Paper accepted to Service Oriented Computing and Applications(SOCA) -
Formal Modeling and Verification of Scalable Service Composition in IoT environment
Sarah Hussein Toman, Lazhar Hamel, Zinah Hussein Toman, Mohamed Graiet, Samir Ouchani
A system based on the Internet of Things (IoT) consists of services deployed across several devices that collaborate to fulfill 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 (QoS), 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 fulfill the requirements of IoT service10 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 proof obligations, and the Rodin prover was responsible for automatically addressing all of these proof obligations.