Titre :	Vérification Formelle de modèles AADL par le modèle checker UPPAAL Etude de cas : contrôleur de température d’un réacteur d’avion
Type de document :	texte imprimé
Auteurs :	Abderrahmane Ayari, Auteur ; Mounira Benyaoub, Auteur ; Alaoua Chaoui, Directeur de thèse ; Med El-Kamel Hamdane, Directeur de thèse
Editeur :	CONSTANTINE [ALGERIE] : Université Frères Mentouri Constantine
Année de publication :	2014
Importance :	77 f.
Format :	30 cm.
Note générale :	Une copie electronique PDF disponible au BUC.
Langues :	Français (fre)
Catégories :	Informatique
Tags :	IDM, AADL, automates temporisés, Uppaal.
Index. décimale :	004 Traitement de données. Informatique
Résumé :	Dans ce mémoire nous allons présenter un travail qui consiste à utiliser les méthodes et outils de l’ingénierie des modèles pour vérifier un système AADL. Ce langage est utilisé dans le cadre de la modélisation des systèmes embarqués temps réel. Notre objectif vise à transformer un modèle AADL vers un modèle formel de type automates temporisés qui sera ensuite exploité par un vérificateur de modèle. Du point de vue développement nous avons utilisé le langage de méta-modélisation Ecore, pour la transformation nous avons exploité le langage ATL. Concernant la vérification, l’outil Uppaal à été choisi. L’ensemble des idées présentées au cours de ce mémoire seront appliquées dans le contexte d’une étude de cas sur un système de contrôleur de température d’un réacteur d’avion.
Diplome :	Master 2
Permalink :	https://bu.umc.edu.dz/master/index.php?lvl=notice_display&id=7828

Vérification Formelle de modèles AADL par le modèle checker UPPAAL Etude de cas : contrôleur de température d’un réacteur d’avion [texte imprimé] / Abderrahmane Ayari, Auteur ; Mounira Benyaoub, Auteur ; Alaoua Chaoui, Directeur de thèse ; Med El-Kamel Hamdane, Directeur de thèse . - CONSTANTINE [ALGERIE] : Université Frères Mentouri Constantine, 2014 . - 77 f. ; 30 cm.
Une copie electronique PDF disponible au BUC.
Langues : Français (fre)

Catégories :	Informatique
Tags :	IDM, AADL, automates temporisés, Uppaal.
Index. décimale :	004 Traitement de données. Informatique
Résumé :	Dans ce mémoire nous allons présenter un travail qui consiste à utiliser les méthodes et outils de l’ingénierie des modèles pour vérifier un système AADL. Ce langage est utilisé dans le cadre de la modélisation des systèmes embarqués temps réel. Notre objectif vise à transformer un modèle AADL vers un modèle formel de type automates temporisés qui sera ensuite exploité par un vérificateur de modèle. Du point de vue développement nous avons utilisé le langage de méta-modélisation Ecore, pour la transformation nous avons exploité le langage ATL. Concernant la vérification, l’outil Uppaal à été choisi. L’ensemble des idées présentées au cours de ce mémoire seront appliquées dans le contexte d’une étude de cas sur un système de contrôleur de température d’un réacteur d’avion.
Diplome :	Master 2
Permalink :	https://bu.umc.edu.dz/master/index.php?lvl=notice_display&id=7828