specification et verification formelles des systemes mecatroniques selon le modele de reference des systemes repartis ouverts rm-odp

Abstract

La mécatronique est la combinaison synergique et systémique de la mécanique, de l'électronique et de l'informatique en temps réel. L'intérêt de ce domaine d'ingénierie interdisciplinaire est de concevoir des systèmes automatiques puissants et de permettre le contrôle de systèmes complexes. Avec la croissance rapide de la technologie, les fonctionnalités proposées par les constructeurs des systèmes mécatroniques sont devenus de plus en plus complexes, ces derniers sont confrontés à de nouveaux problèmes avec ces fonctions, qui dépendent de plusieurs calculateurs et actionneurs répartis sur des réseaux informatiques internes. Dans ce travail nous nous concentrons sur les problèmes d'ingénierie et réingénierie des systèmes mécatroniques. Notre contribution repose sur deux axes, le premier consiste à soumettre à la communauté mécatronique un cadre unificateur, le RM-ODP. Ce cadre est défini comme un méta-standard qui vise à établir des normes qui permettent de tirer profit des avantages de la distribution de l’information dans un environnement possédant des unités hétérogènes de traitement de l’information et qui relèvent de différents domaines d’ingénierie. Dans le deuxième axe, nous proposons une méthode formelle afin de vérifier les lois qui gèrent la sûreté de fonctionnement des systèmes mécatroniques, ces lois sont formalisées en B événementiel. Nous avons construit pas-à-pas une spécification formelle en Event-B d’un système mécatronique. Pour y parvenir, nous avons appliqué une stratégie de raffinement. Une telle stratégie a été appliquée avec succès et a donné naissance à une machine abstraite, des machines raffinées et des contextes. En outre, nous avons validé la spécification formelle obtenue en utilisant avec profit la plateforme RODIN.