Formalisation et vérification de l'interopérabilité dans les systèmes de communication
Institution:
Vandoeuvre-les-Nancy, INPLDisciplines:
Directors:
Abstract EN:
Pas de résumé disponible.
Abstract FR:
Cette thèse traite de la validation de la propriété d'interopérabilité entre un ensemble d'équipements dans les systèmes et applications distribués temps réel. Contrairement au peu de travaux qui ont été déjà menés sur le sujet et qui proposent une validation basée sur la technique de test sur plate-forme, nous avons proposé une méthodologie de validation basée sur une technique de vérification. Etant donné un système composé d'un ensemble d'équipements avec leurs caractéristiques de conformité et un ensemble de processus d'application distribués, la validation de la propriété d'interopérabilité du système par notre approche revient à construire dans un formalisme mathématique le modèle du système et à définir la relation d'interopérabilité en fonction des propriétés régissant la communication puis de vérifier la correction de la relation dans le modèle. L'étude de la problématique a permis de décomposer l'interopérabilité des systèmes de communication selon le modèle OSI et d'identifier quatre classes de caractéristiques des équipements et donc quatre types d'interopérabilité : en services, en protocoles, en ressources et en performances temporelles. L'approche a été concrètement mise en œuvre pour la vérification de l'interopérabilité de services et temporelle à propos d'un système de communication selon le modèle producteur/distributeur/consommateurs. Le système est modélisé et la relation est décrite par des techniques formelles adaptées aux deux types d'interopérabilité