Première année CentraleSupélec 1ère année CS
SIP SIP
Algo Algo
TD 1
- Preuves formelles en Isabelle/HOL des théorèmes du TD.
- Question 2 : parcours en largeur (BFS) avec mémorisation de la profondeur des sommets
- Question 2 : vérification de la profondeur des sommets reliés par une arête.
TD 2 (Plus courts chemins et arbres recouvrants minimaux)
TD 4 (listes et dictionnaires)
- Recherche dichotomique
- Liste chaînée, implémentation avec des dictionnaires
- Liste chaînée, implémentation objet
TD 5 (programmation dynamique)
- Allocation de skis
- Placements financiers
TD 8 (bin packing)
Troisième année Supélec 3ème année
Image Linux Ubuntu 18-04 LTS pour VirtualBox avec tous les logiciels des cours de modélisation et de sémantique :
Cette image contient entre autres :
- Eclipse Oxygen 3a Modeling avec Acceleo et QVT operational
- Isabelle, why3 et krakatoa
Le compte administrateur est ubuntu avec pour mot de passe ModSys3ASI
Modélisation des systèmes Modélisation
7 cours, 1 bureau d'étude (+6 cours et 1 bureau d'étude par Lina Ye)
Objectif
Ce module présente les techniques de modélisation des systèmes qui permettent de concevoir un système informatique, 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 la disponibilité de différents modèles adaptés aux différentes parties d’un système et sur la possibilité d’utiliser conjointement ces modèles.
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. - Modélisation et validation
Ordonnancement, Allocation de ressources (CPU, mémoire). Vérifications formelles: propriétés mathématiques des modèles, preuves, model-checking, application à la sûreté de fonctionnement. - 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 - Hétérogénéité et interactions entre modèles
Hiérarchies de modèles. Problèmes aux limites entre modèles: continu/discret, flots de données/événements. Systèmes modaux. - Application à la modélisation d’un système
Approche réactive synchrone pour le contrôle + preuve formelle, approche à flots de données pour les traitements, temps continu pour la modélisation de l’environnement du système.
Transparents du cours
Les transparents :
- ModSys-00-intro.pdf Introduction, informations sur le déroulement du cours
- ModSys-01.pdf Systèmes, modèles et langages
- ModSys-02.pdf Sémantique des modèles, modèles de calcul
- ModSys-03.pdf Modèles de calcul usuels
- ModSys-04.pdf Automates, parallélisme, approche synchrone
Une version ancienne du polycopié du cours est également disponible.
Logiciels
Vous pouvez travailler sur votre ordinateur pour le cours sur machine et le bureau d'étude. Il suffit pour cela d'installer (configuration validée en octobre 2019) :
- Eclipse IDE 2019-09 https://www.eclipse.org/downloads/ (2019-06 sous Windows)
- Choisissez "Eclipse Modeling Tools" dans l'installer
- Lors du choix du dossier contenant le workspace, évitez les espaces et les caractères accentués dans les noms de dossier, notamment sous Windows
- Après l'installation, lancez Eclipse et ouvrez le market place (menu "Help > Eclipse Marketplace"), sélectionnez le market place Obeo
puis installez Acceleo 3.7
- Redémarrez Eclipse et choisissez "Help > Install new software", puis "Work with: --All Available Sites--" dans le dialogue qui s'ouvre. Sélectionnez :
- Modeling > QVT Operational SDK
- Modeling > QVT Operational SDK Developer Resources
- Modeling > Xtext Complete SDK
- Modeling > Sirius Integration with Xtext
- Si vous souhaitez développer en C++ sous Eclipse, sélectionnez également :
- Programming Languages > C/C++ Development tools
- Programming Languages > C/C++ Library API Documentation Hover Help
- Programming Languages > C/C++ xyz Support (xyz étant votre plateforme : LLVM pour MacOS, Visual C++ for Windows)
- Après l'installation, redémarrez Eclipse. Vous êtes prêt.
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)
Exemples de modèles de systèmes
Quelques exemples de modèles de systèmes réalisés avec Ptolemy II :
Un exemple simple de modèle SDF : une sinusoïde (la porteuse) est modulée par une autre. Le résultat est affiché dans le domaine temporel et dans le domaine fréquentiel.
Ce modèle mixte modélise un cours d'action en bourse, en calcule une moyenne à long terme et une moyenne à cours terme, et utilise un automate pour donner une indication d'achat ou de vente selon l'évolution de ces moyennes.
Sémantique des langages Sémantique
5 cours, 1 bureau d'étude (part de l'évaluation avec les BE de vérification)
Bureau d'étude preuve de programmes avec Krakatoa/Why
Bureau d'étude automates en Isabelle
Livraison de votre travail avec le code ZZPG.
Bureau d'étude sur la sémantique de Niklaus en Isabelle
(Ancienne version du bureau d'étude avec Krakatoa/Why)
Objectif
Ce module présente différentes techniques permettant de définir la sémantique d'un langage de programmation.
Programme
- Syntaxe concrète, syntaxe abstraite
- Syntaxe abstraite et sémantique
- Sémantique traductionnelle
- Sémantique opérationnelle (petits et grands pas)
- Sémantique dénotationnelle
- Sémantique axiomatique
- Sémantique des définitions récursives
- Application au langage Niklaus
À partir de 2015, les définitions sémantiques sont faites en Isabelle/HOL.
Ressources :
- Tutoriel : définition d'un type liste et preuve de théorèmes
- Niklaus : transparents du cours et théories Isabelle pour la définition des différents styles de sémantique du langage Niklaus vu en cours de traitement des langages.
Obsolète depuis septembre 2018
Première année du cursus ingénieur Supélec 1ère année
Architecture des ordinateurs ARCHI
7 cours, 3 séances de travaux dirigés, 2 séances d'études de laboratoire
Voir le site du cours pour plus de détails.
Génie logiciel
Premier TD, nombre secret
Premier BE (TDs 2 et 3)
Version avec la représentation qui utilise une TreeMap de monômes :
Deuxième BE (TDs 4 et 5)
Les résultats présentés ici ont été obtenus avec le modeleur UML Papyrus. Certaines déclarations ont été éditées à la main dans le code Java car la génération de code avec Papyrus n'est pas aussi paramétrable qu'avec RSA.
TD6 (OCL)
