CentraleSupélecDépartement informatique
Plateau de Moulon
3 rue Joliot-Curie
F-91192 Gif-sur-Yvette cedex
Mention « science du logiciel »

Contenu Contact: frederic.boulanger@centralesupelec.fr


COVID-19

En cas de symptôme, ou si vous avez été en contact avec une personne testée positive, vous devez :

Envoyer l'e-mail COVID-19

Rappel des consignes :

Accueil de la mention lundi 21/09/2020 à 9h en F3.03

Les planches

La retransmission sur Teams

Présentation



La mention « science du logiciel » de la dominante « informatique et numérique » a pour objectif de former des ingénieurs par la maîtrise des concepts scientifiques qui permettent de concevoir des systèmes informatiques fiables répondants aux attentes de leurs utilisateurs et de la société. L'enseignement s'appuie en grande partie sur la pratique et sur la mise en œuvre des concepts étudiés sur des cas concrets.

La mention se déroule sur trois séquences, la première étant commune aux quatre mentions (« intelligence artificielle », « science du logiciel », « architecture des systèmes informatiques », et « sécurité ») de la dominante.

Note : HEE = heure équivalent élève, HPE = heure de présence élève. L'objectif est un rapport HPE/HEE compris entre 1/2 et 2/3.

Illustration des problèmes abordés dans cette mention Vidéos

Vidéos de la société Critical Software :

Autres vidéos :

Description générale de la mention Description générale

Cette mention forme des ingénieurs capables de participer à la conception, la réalisation et l'évolution des logiciels qui sont devenus indispensables à la gestion de la complexité des systèmes tant industriels qu’organisationnels. Sont abordées les méthodes (y compris formelles) de spécification, modélisation, conception vérification et validation. Les domaines d'applications couvrent les transports (aérien, spatial, ferré, véhicules autonomes), l'énergie (nucléaire, smart grids, gestion des énergies renouvelables), la santé (imagerie, robots chirurgiens, prothèses), les communications et les systèmes d'information en général (banque, assurance, systèmes industriels, passeports, moyens de paiement et de vote électroniques). Les entreprises visées sont diverses : cabinet de conseil, éditeur de logiciel, ESN, banque, industrie automobile, R&D… Cette mention considère particulièrement :

  • la correction des logiciels (absence de bug), leur sûreté (résistance à des pannes), leur sécurité (protection de leur intégrité et des données), les logiciels pour systèmes critiques (centrales nucléaires, robot chirurgien, véhicule autonome) en vue de leur certification
  • la confiance que l'on peut leur accorder (les décisions qu'ils prennent sont elles conformes à ce qui est annoncé ?), la loyauté des logiciels de démocratie participative, d’admission post-bac...
  • leur évolutivité (interopérabilité, portabilité, extensibilité) : intégration et évolution indépendantes, logiciels pour les infrastructures routières intelligentes faisant appel à différents constructeurs et fournisseurs de services, interconnexion de SI d’entreprises et d’administrations pour l’échange d’informations, continuité des services indépendamment des plateformes (mobiles, tablettes, montres, portables…)

Structure de la mention

En dehors de la séquence commune aux mentions de la dominante (SD9), la mention s'organise en deux séquences d'approfondissement (SG10 et SG11) autour d'un tronc commun de 300HEE et de deux enseignements électifs de 40HEE (un par séquence d'approfondissement).

Tronc commun

Les cours du tronc commun sont regroupés en 5 catégories :

  • Principes de fonctionnement des ordinateurs (40 HEE)
    Logique numérique, processeurs, mémoires, entrées-sorties, interruptions
  • Ingénierie dirigée par les modèles (50 HEE)
    langages, modèles, approches génératives
  • Conception de logiciels sûrs (100 HEE)
    spécification, vérification (test, preuve, analyse statique)
  • Fondements théoriques (80 HEE)
    modèles de calcul, logiques, sémantique
  • Méthodes et outils de conception (40 HEE)
    processus de développement, traçabilité, qualimétrie

Cours électifs (2 x 40 HEE) Électifs

Les enseignements électifs permettent de colorer la formation selon un domaine d’application particulier. Ils constituent d’une part un approfondissement des enseignements du tronc commun et une application à un domaine métier. Il y un enseignement électif de 40 HEE par séquence d’approfondissement de la mention.

En SG10, le choix se fera parmi :

  • Programmation quantique pour le machine learning
  • Analyse formelle de modèles stochastiques (chaînes de Markov, logiques probabilistes)
  • Spécification et test de systèmes temps-réel

En SG11, le choix se fera parmi :

  • Développement de systèmes critiques avec la méthode B
  • SCADE et le synchrone pour les systèmes critiques
  • Algorithmes et modèles pour les systèmes distribués (Hadoop, HDFS, MapReduce)

Séquence commune SD9 (200HEE) Séquence commune

Introduction (10 HEE)

Intervention des parrains de la dominante, conférences

Ateliers de programmation et outils de développement (60HEE/36HPE)

L’objectif de ce cours est de consolider et d’approfondir les compétences en langages de programmation et méthodes de développement (DevOps, intégration continue, tests). D’autre part leur utilisation pour interagir avec un système d’exploitation sera abordée entre autres par la programmation multitâche, et la gestion de la mémoire.

Droit, éthique et vie privée (20HEE/12HPE)

L’objectif de ce cours est de sensibiliser les étudiants aux problématiques de droit en informatique et plus précisément au respect de la propriété intellectuelle et du respect de la vie privée, du respect de la réglementation du RGPD et de son impact sur la transition numérique.

Systèmes concurrents et répartis (40HEE/24HPE)

L’objectif de ce cours est de traiter les calculs distribués, les problèmes de concurrence et de consensus distribués, traités dans le domaine des systèmes répartis. Dans le cadre de ces systèmes, il sera entre autres abordé comment réaliser des calculs sur des données massives.

Modélisation, logiques et modèles formels (40HEE/24HPE)

Ce cours est une courte introduction aux logiques, un des fondements majeurs de l’informatique sur lesquelles se basent les langages et programmes informatiques mais aussi utiles pour la spécification des objets que ces derniers manipulent.

Langages et automates (20 HEE/12HPE)

L’objectif de ce cours est de présenter les bases de la théorie des langages et des automates ainsi que les notions principales sur les compilateurs et qui sont au cœur des notions de calculabilité et de complexité.

Séquence d'approfondissement SG10 (200HE/120HPE) Séquence SG10

Introduction de la mention (10HEE/10HPE)

Ces conférences et séminaires visent à présenter la mention, et à faire intervenir des industriels pour présenter les enjeux types auxquels les élèves seront confrontés, par exemple :

  • systèmes embarqués critiques (maîtrise des risques)
  • aspects sociétaux des algorithmes (transparence et correction des algorithmes)
  • systèmes d’information distribués (fiabilité des réseaux sociaux, systèmes de réservation)

Le déroulement de ces séminaires dépend de l’intervenant : présentation, activités pédagogiques, éventuellement visite d’entreprise si cela soutient le propos.

Principes de fonctionnement des ordinateurs (40 HEE, 24 HPE)

Ce cours présente les principes fondamentaux de fonctionnement des ordinateurs et les illustre par la conception d'un microprocesseur, la traduction d'instructions Python en langage d'assemblage, la gestion des entrées-sorties et les interruptions. Le microprocesseur est réalisé sous Logisim, les entrées-sorties et les interruptions sont présentées sous MicroPython. Ce cours comporte 6h de cours et 15h de pratique, son objectif est d'une part de démystifier le fonctionnement des ordinateurs, et d'autre part d'exposer les mécanismes matériels sur lesquels repose l'exécution des logiciels afin d'avoir conscience des hypothèses faites lors de la vérification de programmes.

Traitement des langages (25 HEE, 15 HPE)

Les langages sont l’outil fondamental de la modélisation des systèmes, de la spécification à la vérification en passant par les différentes étapes de la conception, y compris la programmation. Ce cours présente les concepts fondamentaux du traitement informatique des langages textuels, avec les notions de grammaire, d’analyses lexicale et syntaxique. Il s’appuie sur les outils actuels (ANTLR, Xtext) pour mettre en œuvre ces concepts dans un mini-projet qui se déroule tout au long du cours. Les HPE se décomposent en 4 séances de 3h de cours et une séance de 3h de travaux dirigés permettant le suivi du mini-projet.

Ingénierie des modèles (25 HEE, 15 HPE)

Les modèles sont au cœur de la conception des systèmes, et les modèles informatiques peuvent eux-mêmes être considérés comme des systèmes que l’on modélise, ce qui crée toute une hiérarchie de modèles auxquels s’appliquent les techniques de l’ingénierie des modèles. Ce cours aborde le rôle des modèles, les relations entre modèles, systèmes et langages afin d’éclairer les fondements de l’ingénierie des modèles et de tout l’outillage disponible pour créer des métamodèles, définir des transformations de modèles, valider des modèles. Ces outils sont mis en œuvre et exploités pour limiter les redondances, éviter les incohérences et réutiliser au mieux l’information codée dans les modèles. Un mini-projet sous Eclipse EMF avec QVT-operational et Acceleo se déroule en parallèle du cours, avec une séance de 3h de travaux dirigés pour le suivi. Le cours proprement dit comporte 4 séances de 3h.

Analyse statique (15 HEE, 9 HPE)

L’analyse statique permet de déterminer des propriétés d’un système en examinant ses modèles, sans l’exécuter ni le simuler. Il s’agit d’une approche de la vérification qui est automatique, mais qui peut rapporter de faux positifs (problèmes qui n’existent pas réellement) et passer sous silence des problèmes bien présents (faux négatifs). Ce cours vise à présenter les différentes techniques d’analyse statique, les domaines où elle est la plus pertinente, ses limites et ses avantages.

Systèmes hybrides (15 HEE, 9 HPE)

L'informatique étant souvent utilisée pour contrôler des processus physiques, ce cours met l'accent sur les problèmes qui se posent à l'interface entre le logiciel, discret, et les phénomènes physiques, dont la dynamique est continue.

Test (30 HEE, 18 HPE)

Le test demeure un des piliers de la vérification des systèmes : si on vous donne le choix entre voyager dans un avion prouvé ou dans un avion testé, que choisissez-vous ? Toutefois, les tests coûtent cher, et il est primordial d’assurer le meilleur taux de détection d’erreur par euro dépensé en tests. Ce cours aborde les fondamentaux de la théorie du test, les différents types de tests (unitaire, d’intégration, fonctionnel, fondé sur les modèles etc.), la qualimétrie des tests (taux de couverture), et les méthodes de génération de scénario de test.

Premier cours électif (40 HEE, 21 HPE)

Cours électif à choisir parmi :

  • Programmation quantique pour le machine learning
  • Analyse formelle de modèles stochastiques
  • Spécification et test de systèmes temps-réel

Séquence d'approfondissement SG11 (200 HEE, 116 HPE) Séquence SG11

Logique et modèles de calcul (40 HEE, 24 HPE)

La logique est l’outil de modélisation le plus fondamental. Le choix d’une logique est toutefois un compromis entre pouvoir expressif et décidabilité. De même, la modélisation du comportement d’un logiciel peut s’appuyer sur différents modèles de calculs (automates, réseaux de Petri, machine de Turing, lambda-calcul) parmi lesquels il faut savoir choisir le plus adapté à la résolution d’un problème. Ce cours présente les fondements de la logique : calcul des propositions, logique du premier ordre (prédicats) et logique d’ordre supérieur ainsi que les modèles de calcul sur lesquels reposent les langages de spécification et de programmation. Ces éléments permettront d’aborder la preuve (logique du premier ordre dans la méthode B, logique d’ordre supérieur dans Coq ou Isabelle/HOL). Les algorithmes utilisés par les solveurs SAT et SMT, ainsi que par les assistants de preuve (typage, simplification, méthodes par tableaux) sont également présentés afin de bien comprendre les possibilités et les limitations de ces outils.

Sémantique des modèles et des langages (40 HEE, 24 HPE)

La valeur d’un modèle tient au sens qu’il porte et aux outils qu’on peut lui appliquer. Il est primordial que les différents outils interprètent un modèle donné de la même façon. Ce cours présente les techniques sémantiques qui permettent de définir le sens d’un langage, et donc le sens des modèles exprimés dans ce langage. On y verra comment modéliser la syntaxe abstraite d’un langage (en connexion avec le cours de traitement des langages), choisir un domaine sémantique (en général une logique), et comment établir une correspondance entre les éléments syntaxiques et les éléments sémantiques. Les différents styles de sémantiques (opérationnel, dénotationnel, axiomatique) seront présentés, ainsi que les relations de consistance et de complétude relatives. Ce cours s’appuie sur le cours de logique et modèles de calcul, et suit une approche pragmatique avec une mise en œuvre concrète des concepts et des méthodes dans l’assistant de preuve Isabelle/HOL. 16 heures de travail personnel sont dédiées à la prise en main de l’outil (tutoriel à suivre) et à des exercices. Deux créneaux de 3 heures en présentiel sont consacrés à une pratique encadrée (travaux pratiques) afin d’ancrer les notions abstraites dans leur mise en œuvre concrète sur un cas d’étude.

Preuve (40 HEE, 24 HPE)

La preuve est la certitude la plus absolue que l’on puisse avoir sur la validité d’une propriété d’un modèle. Elle est de plus en plus souvent exigée pour certains algorithmes (même numériques) ou pour le contrôle de systèmes critiques. La preuve peut parfois s’obtenir par exploration exhaustive de l’espace d’états du système (model-checking), mais ce cours s’intéresse à la preuve déductive en général, qu’elle soit trouvée automatiquement par des heuristiques ou qu’elle soit construite pas à pas par un expert. Ce cours permettra de comprendre comment est construit un système déductif, ce qu’est réellement une preuve et comment elle s’obtient. Les concepts seront mis en œuvre sur différents outils afin de donner aux élèves un panorama des techniques disponibles actuellement : Why 3 pour la preuve de programmes et d’algorithmes, Rodin pour la preuve de propriétés en logique du premier ordre, Isabelle/HOL et Coq pour la preuve de propriétés en logique d’ordre supérieur. On verra également comment tirer parti des prouveurs automatiques afin de limiter l’effort humain dans les preuves, et comment rédiger des preuves faciles à maintenir ou à porter d’une modélisation à une autre (preuves structurées).

Méthodes et outils de conception (40 HEE, 24 HPE)

La conception d’un système est un processus complexe qui s’appuie d’une part sur des méthodes scientifiques et des outils, mais également sur des interactions entre êtres humains. L’objectif de ce cours est d’aborder les différentes pratiques de mise en œuvre des outils de conception dans un processus qui prend en compte les facteurs humains et qui permet de contrôler la qualité de la production et la qualité du déroulement du processus. Y seront abordées les méthodes agiles, l’intégration et le déploiement continu, les interactions avec le client pour la définition des besoins, la gestion des exigences etc.

Ce cours sera constitué de diverses interventions au cours de l'année et ne se déroulera donc pas nécessairement durant la séquence 11.

Second cours électif (40 HEE, 21 HPE)

Cours électif à choisir parmi :

  • Spécification, raffinement et vérification avec Event B
  • SCADE et le synchrone pour les systèmes critiques
  • Algorithmes et modèles pour les systèmes distribués