Modèles et vérification pour la composition et la reconfiguration d'applications basées sur le web des objets

The Internet of Things (IoT) applications are built by interconnecting everyday objects over a network. These objects or devices sense the environment around them, and their network capabilities allow them to communicate with other objects to perform utilitarian tasks. One of the popular ways to build IoT applications in the consumer domain is by combining different objects using Event-Condition-Action (ECA) rules. These rules are typically in the form of IF something-happens THEN do-something. The Web of Things (WoT) are a set of standards and principles that integrate architectural styles and capabilities of web to the IoT. Even though WoT architecture coupled with ECA rules simplifies the building of IoT applications to a large extent, there are still challenges in making end-users develop advanced applications in a simple yet correct fashion due to dynamic, reactive and heterogeneous nature of IoT systems.The broad objective of this work is to leverage formal methods to provide end-users of IoT applications certain level of guarantee at design time that the designed application will behave as intended upon deployment. In this context, we propose a formal development framework based on the WoT. The objects are described using a behavioural model derived from the Thing Description specification of WoT. Then, the applications are designed not only by specifying individual ECA rules, but also by composing these rules using a composition language. The language enables users to build more expressive automation scenarios. The description of the objects and their composition are encoded in a formal specification from which the complete behaviour of the application is identified. In order to guarantee correct design of the application, this work proposes a set of generic and application-specific properties that can be validated on the complete behaviour before deployment. Further, the deployed applications may be reconfigured during their application lifecycle. The work supports reconfiguration by specifying reconfiguration properties that allow one to qualitatively compare the behaviour of the new configuration with the original configuration. The implementation of all the proposals is achieved by extending Mozilla WebThings platform. A new set of user interfaces are built to support the composition of rules and reconfiguration. A model transformation component which transforms WoT models to formal models and an integration with formal verification toolbox are implemented to enable automation. Finally, a deployment engine is built by extending WebThings APIs. It directs the deployment of applications and reconfigurations respecting their composition semantics.Les applications de l'Internet des objets (IoT) sont construites en interconnectant les objets du quotidien en réseau. Les objets connectés collaborent ensemble, afin d'observer l'environnement les entourant, et agir sur celui-ci. Pour le grand public, l'un des moyens de créer des applications IoT consiste à combiner différents objets à l'aide de règles d'action conditionnelle (ECA). Ces règles se présentent généralement sous la forme « SI quelque chose se produit, ALORS faire quelque chose ». Le web des objets (Web of Things ou WoT) est un ensemble de normes et de principes qui intègrent les capacités du web et les styles architecturaux à l'IoT. Bien que l'architecture WoT associée aux règles de la ECA simplifie dans une large mesure la construction d'applications IoT, il reste des défis à relever afin que les utilisateurs finaux puissent développer aisément des applications avancées et correctes, en raison de la nature dynamique, réactive et hétérogène des systèmes IoT.L'objectif général de ce travail est de tirer parti des méthodes formelles pour fournir un certain niveau de garantie aux utilisateurs finaux des applications IoT. Cela permet, au moment de la conception, d'assurer que l'application conçue se comportera comme prévu lorsque celle-ci sera déployée. Dans ce contexte, nous proposons un cadre de développement formel basé sur le WoT. Les objets sont décrits à l'aide d'un modèle dérivé de la spécification Thing Description du WoT. Ensuite, les applications sont conçues non seulement en spécifiant les règles individuelles ECA, mais aussi en associant ces règles à l'aide d'un langage de composition. Ce langage permet aux utilisateurs de construire des scénarios d'automatisation plus expressifs. La description des objets et leur composition sont traduites dans une spécification formelle à partir de laquelle le comportement complet de l'application est identifié. Afin de garantir une conception correcte de l'application avant le déploiement, cette thèse propose de valider un ensemble de propriétés génériques et spécifiques sur le comportement complet de l'application. En outre, les applications déployées peuvent être reconfigurées au cours de leur cycle de vie. Le travail supporte la reconfiguration en spécifiant des propriétés de reconfiguration qui permettent de comparer qualitativement le comportement de la nouvelle configuration avec la configuration d'origine. La mise en œuvre de toutes les propositions est réalisée en étendant la plate-forme Mozilla WebThings. Un nouvel ensemble d'interfaces utilisateur est construit pour prendre en charge la composition des règles et la reconfiguration de l’application. Un composant permettant de transformer automatiquement les modèles WoT en modèles formels, pleinement intégré au sein d’une boite à outils de vérification formelle a été développé. Enfin, un moteur de déploiement est construit en étendant les API de WebThings. Il dirige le déploiement des applications et des reconfigurations en respectant la sémantique de leur composition