 |
Résumé :
Les applications IoT déployées dans le continuum IoT–Fog–Cloud doivent concilier des contraintes de ressources, qualité de service (QoS), hétérogénéité et dynamique d’exécution, tout en restant robustes face aux pannes. Dans ce contexte, la fiabilité ne peut pas reposer uniquement sur des tests ad hoc : elle doit être construite et argumentée de manière systématique, depuis les exigences jusqu’au comportement observé en exécution.
Nous présentons d’abord une approche centrée sur la vérification de mécanismes de tolérance aux pannes dans l’IoT multi-couches. La modélisation en Event-B, via raffinement et invariants, permet de formaliser des stratégies telles que la dégradation contrôlée, le basculement vers des composants de secours et la reprise/retour à un état sûr, tout en générant des obligations de preuve garantissant que ces mécanismes préservent les propriétés de sûreté attendues. Cette étape pose un socle : la résilience doit être spécifiée et justifiée rigoureusement, couche par couche, dans des architectures distribuées.
Nous passons ensuite au Fog, où l’enjeu devient la composition de services sous contraintes, depuis les exigences jusqu’au déploiement (et, le cas échéant, l’interaction avec des services cloud). La démarche se décline en étapes : (i) capturer et structurer les exigences (fonctionnelles, coordination, ressources, QoS), (ii) décider un placement correct des composants, (iii) établir une configuration/reconfiguration d’un service composite en arbitrant entre efficacité QoS et fiabilité (notamment transactionnelle), puis (iv) vérifier formellement la cohérence de la composition et des interactions par Event-B. Dans cette dynamique, une perspective consiste à mobiliser des agents conversationnels (systèmes multi-agents conversationnels) pour soutenir l’orchestration et la reconfiguration (négociation de contraintes, adaptation, selection, assistance à la décision), tout en conservant un noyau formel vérifiable.
Enfin, nous motivons une évolution méthodologique : Event-B est très puissant pour prouver des invariants et structurer la correction, mais il n’est pas toujours le plus adapté pour explorer exhaustivement certains comportements dynamiques typiques des systèmes distribués (interleavings concurrents, scénarios d’exécution, blocages, vivacité, effets de reconfiguration). Pour couvrir ces aspects, nous proposons de compléter la preuve par du model checking, en introduisant une transformation Event-B ? Réseaux de Petri Colorés (CPN). Cette transformation vise à obtenir un modèle exécutable et analysable, permettant ensuite d’appliquer des techniques de vérification automatique (exploration d’espace d’états, détection de deadlocks, propriétés de vivacité/atteignabilité) et de refermer la boucle : les contre-exemples et scénarios trouvés alimentent l’amélioration du modèle Event-B, des exigences et des politiques de configuration.
Mots-clés
Continuum IoT–Fog–Cloud, Fiabilité / Résilience, Qualité de service (QoS), Tolérance aux pannes multi-couches, Composition et (re)configuration de services, Placement sous contraintes, Vérification formelle, Event-B, Réseaux de Petri colorés (CPN), Model checking, systèmes multi-agents conversationnels
|