Mémoires de Fin d’Etudes
Etablissement
Université de Biskra - Mohamed Khider
Affiliation
Département d’Informatique
Auteur
MELIOUH, Amel
Directeur de thèse
Chaoui Allaoua (Maitre de conférence)
Filière
Informatique:Programmation et Systéme
Diplôme
Doctorat
Titre
UML et Model-Checking pour la Modélisation et la Vérification des Systèmes Embarqués
Mots clés
Systèmes Embarqués, UML, Maude, Génération de code, Méta-modélisation, ATOM3
Résumé
Ce travail de recherche traite la problématique de vérification formelle des systèmes complexes et plus précisément, les systèmes embarqués. Du fait que ces systèmes sont des systèmes critiques, s’appuyant sur le principe « événement–condition-action » et incluant plusieurs composants, qui interagissent en parallèle, en temps réel, la vérification formelle de ces systèmes devienne une tache très complexe. L’objectif visé est de proposer une approche formelle et automatique pour vérifier les propriétés de ces systèmes, A cet effet, des techniques de transformation de graphes sont abordées. La question qui se pose comment servent t-elles dans la vérification de ces systèmes ? Cette question représente l’ossature de ce projet de recherche et de celle-ci se dégagent plusieurs lignes directrices à savoir : 1- La modélisation automatique des systèmes embarqués par le langage UML en se basant sur la combinaison des diagrammes d’états-transitions et de collaboration. 2- La génération automatique de code écrit en langage Maude à partir des diagrammes UML, utilisant une grammaire de transformation de graphes.. 3- La vérification automatique par le model-Checking des propriétés du système à partir du code généré. Pour réaliser ces trois étapes, j’ai opté pour l’utilisation d’un outil très utilisé dans le domaine de transformation de graphes, basé sur la notion de méta-modélisation et les grammaires de transformation, qui est ATOM3.
Statut
Signalé