Spécification et vérification des systèmes informatiques distribuées conformément au modèle de référence du traitement réparti ouvert (RM-ODP)

Abstract

La conception et le design des systèmes distribués ont besoin d’un Framework structuré afin qu’ils puissent être gérés et contrôlés avec succès. L’objectif du Modèle de référence du traitement réparti ouvert (RM-ODP) est donc de définir ce Framework. C’est dans ce cadre que s’inscrit cette thèse. En effet, elle présente une approche basée sur la sémantique dénotationnelle à partir des spécifications informelles relatives au point de vue traitement et aussi au point de vue ingénierie dans le traitement réparti ouvert (ODP). La sémantique proposée se base aussi sur l’utilisation des langages UML et OCL afin de pouvoir effectuer des vérifications automatiques. Par ailleurs, la composante innovante de notre thèse, qui consiste en l’approche sémantique dénotationnelle, nous a permis d’identifier un sous-ensemble de concepts définis dans la norme RM-ODP et de décrire, en OCL, la formalisation des contraintes statiques et les clauses liées aux concepts d’ODP. En outre, nous avons mis l’accent sur la sémantique des concepts associés aux deux points de vue cités auparavant et de relever les correspondances entre les concepts du comportement du langage de traitement et les concepts du langage BPEL. Pour se faire, nous avons utilisé le ’mapping’ entre UML et BPEL et nous avons ainsi montré l’applicabilité de l’approche proposée. Nous nous sommes intéressés également au problème de l’utilisation d’un outil de preuve Event-B pour des spécifications et vérification de systèmes distribuées. Et enfin, nous avons spécifié une sémantique des concepts de bases de données en utilisant le langage d’ingénierie de RM-ODP.