5 créneaux de 3H, dont 2 de cours, 2 bureaux d'étude, un créneau d'application à un cas d'étude industriel.
Objectif
Ce cours présente les techniques de l'ingénierie dirigée par les modèles qui permettent de concevoir un système logiciel, de simuler son fonctionnement ainsi que l’environnement dans lequel il devra fonctionner, et de générer son code pour une plateforme. L’accent est mis sur systématisation du processus de modélisation et l'utilisation de transformations de modèles pour traiter le raffinement.
Ce cours s'appuie sur les apprentissages du cours de traitement des langages, et sera complété par le cours de sémantique des langages.
Quelques vidéos de la chaîne Computerphile sur le sujet
Un peu de littérature
- Les différents ouvrages de Markus Völter
- Un ouvrage d'Andrzej Wasowski et Thorsten Berger à paraître
Deux exemples de projets utilisant ces techniques
- L'éditeur/assembleur pour MiniARM du cours de PFO
- L'éditeur de code MicroC pour Why3, avec export des lemmes vers Isabelle/HOL (pour le cours de sémantique)
Programme
- Modélisation, abstraction
Modèles et interprétation des modèles. Modèles exécutables, calculables, prédictifs, explicatifs. Modèles classiques: temps continu, temps discret périodique, flots de données synchrones, événements discrets, automates hiérarchiques, systèmes réactifs synchrones. - Ingénierie dirigée par les modèles
Relations entre systèmes, modèles et métamodèles
Définition d'un langage de modélisation (DSL), transformations de modèles
Transparents du cours
Évaluation
L'évaluation est faite sur votre participation aux différentes séances et sur la qualité des travaux rendus :
- exemples faits ensemble en cours
- cours sur machine (automates)
- bureau d'étude (petit langage pour systèmes de transitions)
- cas d'étude avec Theodo
Logiciels
Toutes les manipulations se feront sous Eclipse. Les outils nécessaires sont disponibles dans un conteneur Docker. Ce conteneur vous sera également utile pour les cours :
- Analyse statique (Soufflé)
- Logique (Isabelle, Coq)
- Sémantique des langages et des modèles (Isabelle, Why3)
- Preuve (Isabelle, Coq, FramaC et Metacsl)
Le conteneur peut être lancé facilement à l'aide des scripts start-cs3asl.sh
(sous MacOS ou Linux) et start-cs3asl.ps1
(pour PowerShell sous Windows), disponibles sur ce dépôt GitHub. Pensez quand-même à installer Docker avant...
Installation d'Eclipse
Pour ce cours, vous pouvez aussi installer Eclipse Modeling et éviter les pertes de performances dues à Docker. Je vous conseille de faire une installation d'Eclipse propre à ce cours afin de ne pas risquer de compromettre vos éventuels autres projets utilisant Eclipse. De même, créez un workspace propre à cette installation d'Eclipse.
Je fournis des scripts d'installation d'Eclipse pour Linux, MacOS et Windows sur la page https://wdi.centralesupelec.fr/pfo/EclipseDist.
Ces scripts installent Eclipse Modeling Tools (disponible sur la page des packages Eclipse) avec :
- Acceleo
- OCL Examples and Editors SDK
- Toutes les entrées QVT operational
- Xtext Complete SDK
- C/C++ Development Tools et les plugins associés
- Des plugins liés à XML/XSL et Javascript
- Xtend IDE
Pour vérifier que votre installation d'Eclipse fonctionne, vous pouvez créer un projet :
- Dans le menu "File", choisissez "New Project…"
- Dans le dialogue qui s'affiche, sélectionnez "Ecore Modeling Project" dans le dossier "Eclipse Modeling Framework"
- Après avoir cliqué sur "Next", donnez un nom au projet et cliquez sur "Next" en laissant tous les choix par défaut jusqu'à atteindre la dernière étape où vous cliquerez sur "Finish".
- Vous devriez avoir alors un éditeur de modèles eCore avec une palette d'outils sur la droite.
Sur Mac
Si Eclipse refuse de se lancer, vous pouvez utiliser la commande suivante dans le Terminal pour rendre de nouveau l'application digne de confiance :
sudo codesign --force --deep --sign - /Applications/Eclipse-Modeling-2023-09.app
Il vous faut pour cela les droits d’administrateur. Le nom de l'application est éventuellement à adapter selon la version d'Eclipse que vous avez installée.
Cours sur machine
métamodèles, modèles et transformations de modèle.
Bureau d'étude
Le sujet du bureau d'étude (création d'un DSL)