Présentation
Frédéric Boulanger frederic.boulanger@centralesupelec.fr
Responsable de la mention « Sciences du logiciel »
Recherche
Laboratoire Méthodes Formelles (LMF)
Responsable de la thématique :
« Modélisation formelle des systèmes critiques »
Thèmes de recherche :
- Modélisation des systèmes
- Spécification et vérification
- Aspects temporels, coordination des comportements
Sciences du logiciel
Un socle scientifique
- Modélisation
- Logique, modèles de calcul
- Théorie des langages
Des méthodes pratiques
- Génie logiciel
- Spécification, vérification
- Modélisation, programmation
Pour :
- Concevoir des systèmes : spécifier, modéliser, réaliser, vérifier
- Maîtriser leur complexité
- Orientation logicielle, mais spectre large
Sciences du logiciel
SD9, séquence commune à la dominante
- Droit, éthique et vie privée
- Eco-conception
- Programmation et outils de développement
- Modélisation logique
- Langages et automates
- Algorithmique avancée
Outils et concepts indispensables pour la suite de la mention
Sciences du logiciel
Séquences 10 et 11 spécifiques à la mention
- 420 HEE / 216 HPE en tout
- Alliance de théorie et de mise en œuvre concrète
- Évaluation principalement sur projets et bureaux d'étude
Profils ciblés
- Ingénieurs/chef de projet logiciel en étude ou en R&D
- Expert/consultant en conception de systèmes logiciels
- Compétences en génie logiciel, spécification et vérification
Domaines
- Énergie, transport, défense, santé (systèmes critiques, complexes)
- Banque, assurance (systèmes d'information)
- Startups, ESN (développement, modélisation agile)
- Recherche académique ou industrielle (méthodes de vérification)
Fondements
Comment s'exécute un logiciel ?
- Principes de fonctionnement des ordinateurs (40 HEE)
Du transistor à l'interface matériel/logiciel et aux entrées-sorties
Comment fonctionne un compilateur, un interpréteur ?
- Traitement des langages (30 HEE)
Grammaires, analyse syntaxique, compilation
- Ingénierie des modèles et approches génératives (30 HEE)
Métamodèles, langages spécifiques, interprétation/compilation
Quel sens donner à un modèle ?
- Logique et systèmes déductifs (40 HEE)
Comment exprimer une propriété et raisonner sur un modèle
- Sémantique des modèles et des langages (40 HEE)
Comment donner un sens précis à un langage ?
Génie logiciel et développement
Comment organiser le développement logiciel ?
- Génie logiciel (30 HEE)
Cycles de conception, modélisation objet, patrons de conception
Comment programmer efficacement ?
- Programmation avancée (30 HEE)
Critère de choix d'un langage de programmation, idiomes
Comment concevoir et déployer un logiciel distribué ?
- Algorithmes et modèles pour les systèmes distribués (40 HEE)
Conteneurs, orchestration de services, stockage de données distribué
Conception de logiciels sûrs
Comment intégrer logiciel et équipements ?
- Systèmes hybrides (20 HEE)
Introduction aux spécificités des logiciels
qui pilotent des comportements continus
Comment vérifier des logiciels
- Test (30 HEE)
Comment tester un logiciel et évaluer la qualité des tests
- Analyse statique (20 HEE)
Détecter des erreurs sans exécuter le code
- Preuve de programme (dans le cours de sémantique)
Comment prouver des propriétés d'un logiciel
Cours électif (40 HEE)
En séquence SM10
- Programmation quantique pour le machine learning
- Développement de systèmes critiques avec la méthode B
- Spécification et test de systèmes temps-réels
- SCADE et le synchrone pour les systèmes critiques
Pour approfondir un domaine ou une méthode en particulier.