| Titre : | Spécification et vérification des systèmes embarqués temps réel en utilisant la logique de réécriture |
| Auteurs : | Messaoud Bendiaf, Auteur ; Mustapha Bourahla, 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, 2018 |
| Format : | 1 vol. (150 p.) / 30 cm |
| Langues: | Français |
| Mots-clés: | RT-Maude,systèmes en temps réel,transformation de modèles,grammaires de triples graphes,Interpréteur TGG,modèle-à-texte,spécification et vérification,logique de réécriture,vérification de modèle. |
| Résumé : |
Les systèmes embarqués temps réel doivent être correctement validés et vérifiés avant de les fabriquer et déployer afin d'augmenter leurs fiabilités et de réduire leurs coûts de maintenance. Les modèles sont utilisés depuis longtemps pour construire des systèmes complexes, dans pratiquement tous les domaines de l'ingénierie. C'est parce qu'ils fournissent une aide inestimable pour prendre des décisions de conception importantes avant la mise en oeuvre du système. Dans une activité classique d’Ingénierie Dirigée par les Modèles (IDM), les systèmes sont modélisés à l’aide d’une notation semi-formelle et sont par la suite validés puis implantés. L’étape de validation, basée sur ces modèles, est particulièrement cruciale pour les Systèmes Embarqués Temps-Réel (SETR), afin de s’assurer de leur bon fonctionnement. Cependant, une démarche IDM reste insuffisante dans le sens où elle n’indique pas comment utiliser les modèles pour appliquer l’analyse. Face à cette situation, l’intégration de méthodes formelles dans les cycles de développement de ces systèmes est devenue primordiale. Ces méthodes sont depuis longtemps reconnues afin d’aider au développement de systèmes fiables, en raison de leurs fondements mathématiques, réputés rigoureux sur l’exhaustivité de la vérification formelle qu’ils permettent de l’activer. Dans cette thèse, nous proposons une approche basée sur la transformation de modèle pour obtenir une spécification formelle de notre système, puis utilisons les techniques de vérification formelles pour prouver que la conception de tel système est correcte par rapport à sa spécification. Nous commençons par l’utilisation de diagramme d'états-transitions (Statechart), qui décrit un système temps réel, comme modèle source pour générer un code RT-Maude, ce code représente le module Maude du système temps réel (modèle cible). La deuxième partie de notre travail est de ; en se basant sur le module généré ; vérifier le système par rapport aux propriétés exprimées en logique temporelle linéaire (LTL) en utilisant Maude LTL Model- Checker. En outre, nous utilisons RT-Maude pour rechercher et analyser le système pour trouver des comportements indésirables. L'approche est illustrée à travers trois études de cas. |
| Sommaire : |
1 Introduction générale 1.1 Contexte …………………………..…………………………………………..………… 1.2 Problématique …………………………………………………………………..………. 1.3 Contributions ………………………………………………………………...…...……... 1.4 Organisation du manuscrit .......……………………………………………….....…….... 2 Spécification et vérification des Systèmes Embarqués Temps-réel 2.1 Introduction ……………………………………………………….…………………….. 2.2 Les systèmes embarqués temps réel ………………………………………….…………. 2.2.1 Définitions …………………………….………………………………………. 2.2.2 Système de contrôle/commande temps réel ………………………….……….. 2.2.3 Structure interne d’un système temps réel ……………...………….….……… 2.2.4 Les catégories des systèmes temps réel …………………………….……….… 2.2.5 Caractéristiques des tâches temps réel ………………………….…………….. 2.2.6 Exigences posées par les systèmes temps réel ……………………...………… 2.2.7 Développement classique d’un système embarqué …………...………………. 2.3 Vérification des Systèmes Temps-réel …………………………………...……………... 2.3.1 Modélisation du système ……………………………………...………………. 2.3.2 Spécification Formelle ………………………………………...……………… 2.3.2.1 Techniques descriptives …………………………...………………… 2.3.2.2 Techniques opérationnelles ………………………...……………….. 2.3.2.3 Techniques mixtes ……………………………………...…………… 2.3.3 Vérification Formelle ………………………………………...……………….. 2.3.3.1 Preuve de théorèmes (Theorem proving) ……....…………………… 2.3.3.2 Vérification de modèles (Model-Checking)……...…………………. 2.4 Classification des méthodes formelles ………………………………...………………... 2.5 Méthodes formelles et cycle de vie …………………………………...………………… 2.6 Les formalismes de spécification ………………………………………...……………... 2.6.1 Les automates temporisés ……………………………………...……………… 2.6.2 Les réseaux de Petri ………………………………………………...…………. 2.6.2.1 Propriétés comportementales des RdPs ………………...…………… 2.6.2.2 Les Réseaux de Petri de Haut Niveau ……………………...……….. a) Réseaux de Petri colorés ………………………………….. b) Réseau de Petri Objet …………………………...………... 2.6.2.3 Extensions temporelles des réseaux de Petri …...…………………… a) Les réseaux de Petri temporels ………………...…………. b) Les réseaux de Petri Temporisés …………...…………….. 2.7 Les logiques temporelles ……………………………………………………...………… 2.7.1 Logique temporelle linéaire (LTL) ……………………………………………. 2.7.2 Logique temporelle arborescente (CTL) ……………………………………… 2.7.3 Les logiques temporelles temporisés ……………………………...…………... 2.7.3.1 Extension temporisée de CTL………………………...………….…. 2.7.3.2 Extension temporisée de LTL………………………...…………..… 2.7.4 Choix d’une logique temporelle………………………...…………………..… 2.8 Conclusion ………..……………………………………………………………………... 3 La logique de réécriture comme formalisme de spécification et vérification des systèmes temps réel 3.1 Introduction ……………………………………………...……………………………… 3.2 La logique de réécriture ………………………………………………..……………..… 3.2.1 Théorie de réécriture temps réel …………………………………...………….. 3.2.2 Réflection et stratégie de réécriture ………………………………...…………. 3.2.3 Choix de Maude………………………………………………..……………... 3.3 Maude……………………………………………………………………...……………. 3.3.1 Caractéristiques du langage Maude ………………………………...…………. 3.3.2 Les niveaux de programmation de Maude ………………………….………… 3.3.3 Les modules de Maude ………………………………………………..………. 3.3.3.1 Modules Fonctionnels ……………………………………..………... 3.3.3.2 Modules Systèmes ………………………………………..…………. 3.3.3.3 Modules orientés objet ………………………………..…………….. 3.3.3.4 Modules prédéfinis …….…………………………………..………... 3.4 Real-Time Maude……………………………………………...………………………... 3.4.1 Les Modules Temporisés (Timed modules) ……………………………..……. 3.4.1.1 Les Domaines de Temps (Time Domains) ……………….…………. 3.4.1.2 Les règles Tick ………………………………………..…………….. 3.4.2 Exemples de Modules Temporisés : Modélisation d’une horloge ……….…… 3.5 Analyse formelle et vérification des propriétés avec Maude …………………..……….. 3.6 Conclusion ……………………………………………………………………...……….. 4 La modélisation avec UML 4.1 Introduction ………………………………………………...…………………………… 4.2 La modélisation …………………………………………...…………………………….. 4.2.1 Les types de modélisation ………………………………..…………………… 4.2.1.1 Modélisation Informelle …………………………..………………… 4.2.1.2 Modélisation Semi-Formelle ………………………..………………. 4.2.1.3 Modélisation Formelle ………………...…………………………….. 4.2.2 La Modélisation Orientée Objet ………………………………..……………... 4.3 Historique des méthodes de conception …………………………………..…………….. 4.4 UML (Unified Modeling Language)…………………………………...……………….. 4.4.1 Les diagrammes UML…………………………………………...……………. 4.4.2 Extensions d’UML………..…………………………………………………... 4.4.2.1 Stéréotypes ……...….…………………..…………………………… 4.4.2.2 Valeurs étiquetées (tagged values) …………..……………………… 4.4.2.3 Le langage de contraintes OCL (Object Constraints Language) ….… 4.4.3 Vues et diagrammes UML………………………….………………………… 4.4.4 UML et Cycle de développement ……………………………..………………. 4.4.5 Diagramme d’états-transitions ………………………………..………………. 4.5 Processus de développement ………………………………………..…………………... 4.5.1 Méthode Processus Unifié (UP) ……………………………………..……...… 4.5.2 Méthode 2 Tracks Unified Process (2TUP) …………….…………………….. 4.6 Conclusion …………………………………………...………………………………….. 5 Ingénierie Dirigée par Modèles (IDM) 5.1 Introduction ……………………………………...……………………………………… 5.2 Ingénierie Dirigée par Modèles (IDM) ………………………………….……………… 5.2.1 Niveaux d’abstraction ………………………………...……………………….. 5.2.2 Critères d’un bon modèle ………………………..……………………………. 5.2.3 Transformations de modèles …………………….......….………..…………… 5.2.3.1 Les approches de l’ingénierie dirigée par les modèles …….………... a) Transformations de type Modèle vers code …………..…………... a.1) Les approches basées sur visiteur ………….…………… a.2) Les approches basées sur Template …………..………… b) Transformations de type modèle vers modèle …………..………... b.1) Approches manipulant directement les modèles ….……. b.2) Approches relationnelles ………………..……………… b.3) Approches guidées par la structure ………..……………. b.4) Approches basées sur la transformation de graphes ….… b.5) Approches hybrides ……………………..……………… 5.2.3.2 Les activités de la transformation de modèles ………………….…… 5.2.3.3 Propriétés d’une transformation de modèles ……………….……….. 5.2.3.4 Les avantages de l’IDM …………………………...………………… 5.3 L’approche MDA (Model-Driven Architecture) ……………….………………………. 5.3.1 Standards et espaces techniques …………………………………..…………... 5.3.2 Types de modèles dans MDA …………………………………..…………….. 5.3.3 Passage entre modèles …………………………………………..…………….. 5.3.4 Types de transformations de modèles dans MDA ………………..…………… 5.3.5 Technologies ……………………………………..…………………………… 5.3.5.1 Méta Object Facility (MOF) ……………………………..………….. 5.3.5.2 XMI (XML Metadata Interchange) ……………………..…………... 5.3.5.3 CWM (Common Warehouse Metamodel) ………………….………. 5.3.5.4 QVT (Query/View/Transformation) ……………………..…………. 5.4 Autres approches centrées sur les modèles …………………………………….……….. 5.4.1 Computer Aided Software Engineering (CASE) ……………………..………. 5.4.2 Model Integrated Computing (MIC) ……………………………..…………… 5.4.3 Software Factories ……………………………………………..……………… 5.5 Principe de transformation de graphes ……………………………………..…………… 5.5.1 Notion de Graphe ………………………………..……………………………. 5.5.2 Grammaire de Graphe ……………………………………..………………….. 5.5.2.1 Le principe de règles ………………………………..………………. 5.5.2.2 Application des règles ……………………………..………………... 5.5.2.3 Système de transformation de graphes ………………..…………….. 5.5.2.4 Langage engendré .…………………………………...……………… 5.5.3 Outils de transformations de graphes …………………….…………………… 5.6 Conclusion ………………………………………...…………………………………….. 6 Contributions 6.1 Introduction ………………………………………………………………...………….. 6.2 Outils d’implémentation ………………………………………...……………………... 6.2.1 La plateforme Eclipse ……………………………………..…………………. 6.2.2 EMF/Ecore…………………………………………...………………………. 6.2.3 TGG Interpreter ……………………………………………………..……….. 6.2.4 Le langage de génération de code Xpand ……………………….…………… 6.2.4.1 Structure générale d’un template Xpand ………………..………….. 6.2.4.2 Structure générale d’un Workflow…………………...…………….. 6.2.4.3 Langage XTEND …………………..………………………………. 6.2.4.4 Le langage Check ………………………………………………...… 6.3 L'approche proposée ……………………………………………...……………………. 6.3.1 Transformations de modèle à modèle (M2M) …………………………..…… 6.3.1.1 Les métamodèles impliqués ………………………………...……… 6.3.1.2 Définition des règles de TGG ………………………..…………….. 6.3.2 Transformations de modèle à texte (M2T) ………………………...………… 6.4 Conclusion ………………………………………………………...…………………… 7 Études de cas 7.1 Introduction ……………………………………………...…………………………….. 7.2 Études de cas …………………………………………..………………………………. 7.2.1 Feu de circulation tricolore …………………………………………………... 7.2.1.1 Modélisation …………………………………………..…………… 7.2.1.2 L’exécution de grammaire ……………………..…………………... 7.2.1.3 Génération de code …………………………………………………. 7.2.2 Thermostat …………………………………………...………………………. 7.2.3 Robot industriel ………………………………………………………………. 7.3 Analyse et vérification formelle ……………………………………...………………... 7.3.1 Feu de circulation tricolore ………………………………………………....... 7.3.1.1 Réécriture temporisée (Timed Rewriting) ………………..………... 7.3.1.2 Recherche temporisée (Timed Search) ……………………..……… 7.3.1.3 Recherche non temporisée (Untimed Search) …………...…………. 7.3.1.4 Vérification via le model-checker LTL…………………………….. 7.3.2 Thermostat …………………………………...………………………………. 7.3.2.1 Réécriture temporisée (Timed Rewriting) ……………...………….. 7.3.2.2 Recherche temporisée (Timed Search) ………………..…………… 7.3.2.3 Recherche non temporisée (Untimed Search) …………..………….. 7.3.2.4 Vérification via le model-checker LTL…………………………….. 7.3.3 Robot industriel ………………………………………………………………. 7.3.3.1 Réécriture temporisée (Timed Rewriting) ……………………...….. 7.3.3.2 Recherche temporisée (Timed Search) ………………..…………… 7.3.3.3 Recherche non temporisée (Untimed Search) ………...……………. 7.3.3.4 Vérification via le model-checker LTL…………………………..… 7.4 Expérimentations et Résultats …………………………………………..……………... 7.5 Conclusion ……………………………………………………...……………………… Conclusion générale …………………………………………………………………….… Bibliographie ……………………………………………………………………………… |
| En ligne : | http://thesis.univ-biskra.dz/id/eprint/3759 |
Disponibilité (1)
| Cote | Support | Localisation | Statut |
|---|---|---|---|
| TINF/121 | Théses de doctorat | bibliothèque sciences exactes | Consultable |
