Formalisation des modèles d'information d'administration de réseaux à l'aide de la méthode B : Application au langage GDMO / par David Watrin ; sous la direction de Tayeb Ben Meriem

Date :

Editeur / Publisher : [S.l.] : [s.n.] , 2001

Type : Livre / Book

Type : Thèse / Thesis

Langue / Language : français / French

Ben Meriem, Tayeb (19.. ; Professeur) (Directeur de thèse / thesis advisor)

Télécom Paris (Palaiseau ; 1977-....) (Organisme de soutenance / degree-grantor)

Résumé / Abstract : Suite à la libéralisation des marchés de télécommunications et à la multiplication de l'offre de services, l'Administration de Réseaux de Télécommunications connaît un réel essor. A l'exception de SNMP, les différentes technologies qui adressent cette activité ont fait le choix de langages orientés objets afin de décrire leurs modèles d'information. Ce choix est motivé par des considérations d'évolutivité bien connues. Cependant une constante se dégage à travers ces langages: I'utilisation du langage naturel pour décrire les contraintes et les comportements des objets gérés, des attributs et autres "templates". Ce choix induit l'introduction d'ambigui͏̈tés dans la spécification et n'autorise pas de traitement automatique afin de simuler ou tester le comportement, de vérifier la cohérence du modèle ou de produire un code exécutable. Enfin les modèles sont difficiles à appréhender en raison d'une distribution anarchique de l'inforrnation. Ce travail de thèse propose une solution basée sur la formalisation des modèles à l'aide de la méthode B. Cette dernière offre en effet un langage rigoureux et automatise les concepts de preuve formelle et de raffinement. Afin de définir une solution générique, les propriétés communes aux modèles d'information de gestion de réseaux ont été isolées. Un ensemble de règles de traduction vers le formalisme B couvrant les structures de données et les modèles statique et dynamique est proposé. Des variantes sont avancées et analysées lorsque aucune règle n'est pleinement satisfaisante. Ces règles ont été appliquées avec succès à un modèle GDMO. La spécification B obtenue permet de prouver la cohérence interne du modèle et d'amorcer le processus de raffinement. En outre, un traducteur automatique depuis un modèle GDMO vers une spécification B a été développé. Il offre une large couverture du langage et permet de saisir des propriétés formelles via une interface graphique. Il contribue à un enrichissement du modèle d'information.