Informations
Directeur de thèse :
Année de début :
Fin 2009
Université :
Université Constantine 2
Soutenance
Date de soutenance :
14 Mai 2018
Jury :
Faiza Belala
Allaoua Chaoui
Salah Hamri
Elkamel Merah
Salah Merniz
Manuscrit
Téléchargement :
Détails
Titre :
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étamodè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é. Une étude de cas a été développé pour démontrer la faisabilité et la validité de l’approche proposée.


Mots clés :
AADL Automate temporisé Transformation de modèle Vérification Uppaal


Abstract:

In this work, we propose an approach for the verification of the AADL Architecture and Analysis Design Language) description. This approach is based in Model Driven Engineering (MDE) and assisted by a toolchain. Indeed, we define a source meta-model for AADL and a target meta-model for the timed automata formalism; we define a transformation process in two steps: the first is a Model2Model transformation which takes an AADL Model and produces the corresponding timed automata model. The second transformation is a Model2Text transformation which takes a timed automata model and generates a text in ta-format code. This code is accepted by the Uppaal toolbox. The goal of this effort is to insure some properties of AADL models using the Uppaal model checker. A case study has been developed to show the feasibility and validity of the proposed approach.


Keywords:
AADL Timed Automata Model Transformation Verification Uppaal