Une approche basée sur l’ingénierie dirigée par les modèles pour la vérification des descriptions AADL.

Résumé

Dans ce travail, nous proposons une approche pour la vérification des descriptions AADL (Architecture and Analysis Design Language). Cette approche est basée sur l’ingénierie dirigée par les modèles (IDM) et assistée par un ensemble d’outils. En effet, nous proposons un méta-modèle source pour AADL et un méta-modèle cible pour le formalisme des automates temporisés. Puis, nous définissons un processus de transformation en deux étapes ; la première est une transformation de type Model2Model qui prend un modèle AADL en entrée et produit le modèle d’automates temporisés correspondant en sortie. La deuxième étape est une transformation de type Model2Text qui prend le modèle généré dans la première étape et le transforme en texte dans le code “ta-format”. Ce code est une représentation textuelle interne du model-checker UPPAAL. L’objectif de cette initiative est d’assurer certaines propriétés des modèles AADL comme l’absence de l’interblocage, la sûreté et la vivacité. Deux études de cas ont été développé pour démontrer la faisabilité et la validité de l’approche proposée.

Citer ce document

Accès au document

Ce document est hébergé sur son dépôt institutionnel d'origine.

Auteur(s)

Statistiques

Consultations : 2

Téléchargements : 0