Formal Verification of Control and Operational Behaviors in Industrial Internet of Things Services Composition

Industrial Internet of Things (IIoT) services composition rely on composing existing IoT services in industrial context in order to obtain an overall service with added value. The composite service's behavior is extremely influenced by the time, availability, and accuracy of the unitary services. Thus, it is extremely important to guarantee a provision of IIoT services as expected during the modeling phase. For this, we lie on formal verification to check all the possible scenarios before to pass through IIoT services provision. We propose first to model each process involved in the composition by open Time Petri Nets. These nets offer interface places for the purpose of process communication with the other processes. Then the composition of open Time Petri Nets is guaranteed via superimposing the interface places and thus obtaining a Time Petri Net modeling the composite process. Finally, control and operational behaviors of IIoT services composition formally checked after being specified in an expressive fragment of TCTL temporal logic.