A Formal Modeling and Verification Approach for IoT-Cloud Resource-Oriented Applications
Résumé
IoT-Cloud environments are being increasingly adopted for the deployment of applications and particularly resource-oriented ones. However, ensuring correct communications during the execution of IoT applications is not guaranteed. In fact, a substantial class of applications is intended to run on constrained IoT networks. Moreover, IoT devices exchange the data derived from various Cloud providers and in accordance with different protocols. In this paper, we propose a formal approach to model and verify the applications deployed over IoT-Cloud environments. The proposed model encompasses four verification levels: the Structural, Functional, Operational and Behavioral levels. Therefore, we opted for the Event-B formal method that allows gradual problems decomposition by relying on its refinement capabilities. The proposed approach has proven its efficiency for the modeling and the verification of IoT applications. We applied mathematical proof-based method to verify the model since it provides rigorous reasoning. We also employed the ProB animator to proceed in the validation of the model.
| Origine | Fichiers produits par l'(les) auteur(s) |
|---|
