| Titre : | UML et Model-Checking pour la Modélisation et la Vérification des Systèmes Embarqués |
| Auteurs : | Amel Meliouh, Auteur ; Allaoua Chaoui, Directeur de thèse |
| Type de document : | Thése doctorat |
| Editeur : | Biskra [Algérie] : Faculté des Sciences Exactes et des Sciences de la Nature et de la Vie, Université Mohamed Khider, 2021 |
| Format : | 1 vol. (111 p.) / couv. ill. en coul / 30 cm |
| Langues: | Français |
| Mots-clés: | UML,Real-Time Statechart diagram,Real-Time Collaboration diagram,génération de code,Méta-modélisation,Grammaire de graphes,ATOM3,MITL,Model checking,language Maude |
| Résumé : |
Ce travail présente une approche formelle de modélisation et de vérification des systèmes embarqués. L’approche repose sur une modélisation du comportement temporel du système et une génération automatique de code. Le concept clé est l'utilisation combinée d'un ensemble de diagrammes comportementaux d’UML étendu par des annotations temporelles (diagrammes Statechart temps réel et de collaboration temps réel) pour la modélisation du système et le langage Maude pour la vérification. Tout d'abord, un outil de modélisation UML est développé, ensuite, une grammaire de graphes est exécutée pour générer automatiquement des spécifications en Maude équivalentes. L'approche repose sur la génération de code, donc il est possible d'utiliser un outil de vérification de modèles (Model-cheking) pour vérifier certaines propriétés temporelles représentées dans la logique temporelle temps réel (MITL). |
| Sommaire : |
Introduction Générale Contexte général………………………………………………………………… 1 Problématique ………………………………………………………………….. 2 Etude des travaux réalisés……………………………………………………… 5 Contribution…………………………………………………………………….. 5 Structure du manuscrit………………………………………………………… 6 Chapitre 1: Modélisation et vérification des systèmes embarqués 1. Introduction………………………………………………………………….. 9 2. Les systèmes embarqués…………………………………………………….. 9 2.1 Définitions………………………………………………………………….. 9 2.2 Caractéristiques d’un système embarqué………………………………… 11 2.3 Architectures des systèmes embarqués…………………………………… 12 2.3.1 Les architectures centralisées…………………………………………. 13 2.3.2 Les architectures réparties……………………………………… ……. 13 2.3.3 Les architectures fédérées……………………………………… ……. 13 2.4 Structure générale d’un système embarqué………………………………. 14 2.5 Les systèmes embarqués et le temps réel…………………………… ……. 15 2.6 Les exigences de développement des systèmes embarqués………………. 16 2.6.1 Besoins de modèles à la fois locaux et globaux……………………….. 16 2.6.2 Déterminisme…………………………………………………………… 17 2.6.3 Vérification……………………………………… ……………………. 17 2.6.4 Le problème de la modification par “delta”………………………….. 17 3. Approches de Développement des Systèmes Embarqués…………………... 18 3.1 Développement Classique……………………………………………. ……. 19 3.1.1 Principe générale………………………………………………… ……. 19 3.1.2 Discussion………………………………………………………………. 21ix 3.2 Développement niveau système……………………………………………. 21 3.2.1Synthèse niveau système……………………………………………………. 22 3.2.2Conception basée plateforme………………………………………………. 22 3.2.3Conception basée modèle………………………………………….. ……. 23 3.2.4Conception basée architecture……………………………………… …… 23 3.2.5Discussion…………………………………………………………………… 24 4. Langages de modélisation des systèmes embarqués……………………….. 24 4.1 AADL (Architecture Analysis & Design Language)…………………….. 24 4.2 Profile MARTE (Modeling and Analysis of Real-Time Embedded systems).. 25 4.3 SysML………………………..………………………..……………………. 26 4.4 UML………………………..………………………..……………………… 27 4.5 Spécification PEARL et le profil UML-RT………………………………. 27 4.6 Discussion………………………..………………………..………………… 28 5. Vérification des systèmes embarqués……………………………….………. 28 5.1 Vérification par simulation……………………………….……………….. 29 5.2 Vérification formelle……………………………….……….……………… 30 5.2.1 Techniques de vérification formelle……………………………….….. 31 5.2.2 Apports des méthodes formelles……………………………….……… 34 5.3 Discussion……………………………….……….…………………………... 35 6. Conclusion……………………………….……….……………………………. 36 Chapitre 2: Ingénierie dirigée par les modèles 1. Introduction……………………………….……….…………………………. 38 2. Ingénierie dirigée par les modèles (IDM) ……………………………….…. 38 2.1 Présentation……………………………….……….………………………... 38 2.2 Notions de Modèle et Méta-modèle……………………………….………. 39 2.3 Transformation de Modèles……………………………….……….……… 40 2.4 Manipulations des modèles……………………………….……….………. 42 2.4.1 Réalisation de modèles……………………………….……………….. 42 2.4.2 Stockage de modèles……………………………….………………….. 42 2.4.3 Echange de modèles……………………………….…………………... 42 2.4.4 Exécution de modèles……………………………….………………… 42x 2.4.5 Vérification de modèles……………………………….……………… 43 2.4.6 Validation……………………………….…………………………….. 43 2.4.7 Gestion de l’évolution des modèles……………………………….…... 43 2.5 Les approches de l’Ingénierie dirigée par les modèles……………………. 44 2.5.1 L’Architecture Dirigée par les Modèles (MDA) ……………………... 44 2.5.2 Standards de l’OMG……………………………….…………………... 44 2.5.3 Les différents modèles du MDA ……………………………….…… 45 2.5.4 Transformations de modèles dans MDA……………………………… 46 2.5.5 Le principe de transformations de modèles………………………….. 47 2.5.6 MOF et L’architecture à quatre niveaux…………………………….. 49 2.6 Processus de Vérification en IDM……………………………….………… 50 3. Les méthodes formelles de vérification……………………………….……... 51 3.1 Les langages formels……………………………….………………………. 51 3.2 Techniques d’analyse……………………………….……………………… 52 3.2.1 Vérification……………………………….……………………………. 52 3.2.2 Validation……………………………….……………………………… 52 3.2.3 Qualification……………………………….…………………………… 52 3.2.4 Certification……………………………….…………………………… 52 3.3 Techniques de vérification formelle………………………………………. 53 3.3.1 Vérification de Modèle (Model Checking) …………………………... 53 3.3.2 Preuve de théorèmes (Theorem proving) …………………………… 54 4. Combinaison d’IDM avec les Méthodes Formelles………………………... 54 5. Conclusion ……………………………………….…………………………. 56 Chapitre 3: La logique de réecriture et le langage Maude 1. Introduction……………………………………….…………………………. 59 2. Logique de Réécriture………………………………………………………. 59 3. Système Maude……………………………………….……………………... 60 3.1 Modules fonctionnels……………………………………………………… 61 3.2 Modules Systèmes.................................................. 63 3.3 Modules orientés objet……………………………………………………. 63 4. Modules prédéfinis……………………………………….…………………. 65xi 5. Exécution et analyse formelle sous Maude………………………………… 66 6. Analyse formelle et vérification des propriétés ………………………….. 66 6.1 Logique temporelle linéaire (LTL) ……………………………………… 67 6.2 Le Model Checker LTL de Maude………………………………………… 68 7. Exécution de Maude……………………………………….…………………. 70 8. Conclusion……………………………………….……………………………. 72 Chapitre 4: Une approche et un outil de modélisation et de vérification des systèmes embarqués 1. Introduction……………………………………….…………………………. 74 2. Comportement temporel d’un système…………………………………….. 75 3. Les diagrammes d’états -transition et de communication temps reel…… 76 3.1 Les diagrammes d’états-transitions temps réel…………………………… 76 3.2 Les diagrammes de collaboration temps réel……………………………… 77 4. Méta-modélisation des RTSTs et RTCs……………………………………… 78 4.1 Méta-modèle des RTSTs……………………………………………………. 78 4.1.1 Les associations………………………………………………………… 79 4.1.2 Les classes……………………………………….……………………… 80 4.2 Méta-modèle des RTCs……………………………………….…………….. 83 5. Génération du code Maude équivalent………………………………………. 85 5.1 La grammaire de transformation……………………………………….…. 85 6. Vérification des propriétés temporelles d’un système embarqué………….. 92 6.1 Modélisation avec ATOM3……………………………………….………… 93 6.2 Génération du code en Langage Maude…………………………………… 94 6.3 Vérification d’une propriété temporelle…………………………………… 95 6.3.1 Logique temporelle Temps réel………………………………………… 96 6.3.2 Définition d’une propriété temporelle………………………………… 99 7. Conclusion……………………………………….…………………….……… 101 Conclusion Générale…………………………………………………………… 103 Bibiographie……………………………………………………………………. 105 |
| En ligne : | http://thesis.univ-biskra.dz/id/eprint/5366 |
Disponibilité (1)
| Cote | Support | Localisation | Statut |
|---|---|---|---|
| TINF/156 | Théses de doctorat | bibliothèque sciences exactes | Consultable |
