Méthode B pour la spécification et la vérification formelle des systèmes répartis ouverts

Abstract

Le modèle de référence pour le traitement réparti ouvert (RM-ODP) fournit un cadre dans lequel le support de la distribution, l'interfonctionnement et la portabilité peuvent être intégrés. Cependant, la sémantique de ses langages de points de vue est informelle. Notre objectif est de contribuer à la précision de la sémantique des concepts de base du système ODP permettant ainsi de construire correctement ces systèmes. Pour la spécification des concepts ODP, les langages Z, SDL, LOTOS, et Estelle sont utilisés dans la sémantique architecturale de RM-ODP. Toutefois, aucune méthode formelle n’est susceptible d'être adaptée pour spécifier tous les aspects d'un système ODP. Dans ce contexte, nous avons proposé l’utilisation de la méthode event-B tirant ainsi profit de la puissance de cette méthode afin d’aboutir à des systèmes ODP corrects par construction. Nous avons d’abord utilisé la méthode event-B pour la spécification précise des politiques ODP du point de vue entreprise. Puis, nous avons présenté une approche formelle pour la modélisation et l'analyse de la fonction de courtage en utilisant event-B. Enfin, nous avons développé le processus de négociation de la qualité de service nécessaire pour la coopération entre les objets. La Plate-forme Rodin pour event-B fournit un support efficace pour le raffinement et la preuve mathématique. Nous avons utilisé cette plate forme pour vérifier l’exactitude des machines B conçues.