SCHOOL INGÉNIERIE, STI

MASTER Informatique Parcours FIIL

Fondements de l'informatique et ingénierie du logiciel

Les problématiques abordées dans le parcours FIIL

		Quels outils utiliser pour savoir si mon logiciel a des bugs ou garantir qu'il n'en a pas ? Comment fonctionnent ces outils ?
Comment les algorithmes de Google, Facebook, etc. fonctionnent-ils ?
		Comment sont programmées les applications web, système ou réseaux avancées ? Avec quels langages de programmation ?
Quels algorithmes ou paradigmes de programmation permettent d'utiliser au mieux les architectures modernes des ordinateurs afin d'optimiser mes calculs (gain de performance, minimisation énergie) ?
		Quels algorithmes ou quelles structures de données utiliser pour résoudre des problèmes combinatoires ou d'optimisation?
Quels méthodes et outils utiliser pour modéliser mathématiquement des systèmes complexes (afin de raisonner et prouver des propriétés) ?

Présentation

Ce parcours propose un cursus d'informatique fondamentale et d'ingénierie du logiciel principalement aux étudiants issus d’un M1 informatique et aux étudiants ingénieurs. Il constitue aussi une initiative structurante proposant une offre cohérente de formation qui fédère plusieurs acteurs et réunissant des écoles d'ingénieurs et des Universités. La formation présentera les fondamentaux dans les domaines des méthodes et des langages formels, de la modélisation, de l’optimisation, de l’algorithmique et la programmation. Elle offrira également un parcours professionnalisant sur l'ingénierie du logiciel s'appuyant sur des techniques modernes de développement de projets. Elle se distinguera par une politique pédagogique fondée sur la pratique par projets et l'usage des méthodes et outils issus de travaux menés par les laboratoires de recherche et ceux utilisés actuellement dans l'industrie du logiciel.

La formation vise, dans un esprit d'ingénierie, à ancrer concepts fondamentaux, connaissance et compréhension par la confrontation à la situation pratique, cette dernière donnant une forme du recul sur la problématique. Les étudiants seront ainsi amenés à maîtriser conjointement les fondements théoriques des thèmes abordés et les atouts et limitations de leur déclinaison outillée.

Débouchés

La formation permettra de s'insérer efficacement dans le monde industriel et de s'adapter aisément aux nouvelles technologies et environnements de développement. Elle ouvrira également des opportunités de carrières publiques ou privées dans le domaine de la recherche et de l'innovation. Les étudiants souhaitant faire une thèse auront la possibilité de la faire soit dans un laboratoire de recherche, soit en R&D/R&I dans des centres de recherche industriels.

Programme du parcours

Le master est composé de 20 unités d'enseignements (UE) de 2.5 crédits. Chaque étudiant doit en choisir 12 pour valider le premier semestre. Le second semestre est entièrement consacré au stage (30 ECTS). L'emploi du temps est disponible à l'adresse suivante.

Nous vous invitons à remplir le formulaire suivant pour indiquer vos choix d'UE.

Liste des UE (toutes à 2.5 ECTS)

UE 1 : Langages centrés données (Kim Nguyen)

L'objectif de cette UE est de présenter des aspects de compilation et de théorie des langages (au sens large) spécifiques aux langages centrés données.

UE 2 : Test fonctionnel de protocoles (Fatiha Zaïdi, Stéphane Maag)

Dans cette UE nous mettrons l'accent sur la mise en oeuvre de techniques pour générer des ensembles de tests permettant de couvrir des objectifs de test. La notion d'objectif de test peut correspondre à plusieurs notions concrètes incluant des propriétés à tester, des contrats, des comportements sous forme de chemins à couvrir , des critères de couvertures portant sur les graphes de contrôles ou les flots de donnés.

UE 3: Calcul Haute Performance (Marc Baboulin)

L'objectif de ce cours est de donner une vision détaillée des algorithmes et paradigmes de programmation parallèle rencontrés dans le calcul scientifique haute-performance et de leur utilisation sur les architectures matérielles les plus récentes. Thèmes abordés : Nous décrirons les principaux défis matériels et logiciels rencontrés dans les simulations de très grandes tailles effectuées dans l’industrie et la recherche scientifique. Nous présenterons les principes essentiels de conception d’algorithmes parallèles en utilisant les modèles de programmation des machines multi-processeurs (mémoire distribuée, partagée, accélérateurs, extension vectorielle…). Nous aborderons les problématiques essentielles liées à l’équilibrage de charge ainsi qu’à la minimisation de l'énergie et du coût des communications et des synchronisations. Les différentes méthodes de programmation seront illustrées par des exemples d'application variés (e.g., reconstruction d'image, comportements énergétiques…).

UE 4 : Vérification/Preuves interactives et applications (Burkhart Wolff)

La preuve interactive de théorèmes est une technologie qui prend une place de plus en plus importante tant en informatique qu’en mathématiques. Elle s’appuie sur des langages logiques d’une grande expressivité et des implantations garantissant le plus haut niveau de confiance. Parmi les applications, on notera la preuve du théorème de Feit-Thompson, un résultat avancé en théorie des groupes finis ou encore la preuve semi-automatisée de seL4, un noyau sécurisé de Linux correspondant à un système logiciel complexe. Ce cours est une introduction aux concepts fondamentaux des environnements de preuves interactives de théorèmes et sera illustré par l’apprentissage du système Isabelle/HOL. Les exemples porteront sur la modélisation et la preuve de certains aspects des systèmes critiques ainsi que sur l’utilisation des outils de preuves interactives pour modéliser et prouver des propriétés de langages ou de systèmes logiques.

UE 5 : Comptage et énumération de structures de données (Florent Hivert, Viviane Pons)

UE 6 : Langage : sémantique et modèles d'exécution (Thibaut Balabonski)

UE 7: Programmation d'applications Web avancées (Kim Nguyen, Fatiha Zaïdi)

Développement d'applications et de services Web complexes : traitements complexes coté client (suite du M1), environnements (framework) coté serveurs (Apache struts, Ocsigen, ...), intégrations de données hétérogènes (BD, XML, Json, ...), programmation de services Web (SOAP, REST).

UE 8 : Programmation systèmes et réseaux (Steven Martin)

Introduction aux réseaux Ad-hoc sans fil sous GNU/Linux et au développement sur systèmes embarqués Description. Ce module forme les étudiants à la programmation système et réseau dans un environnement TCP/IP pour l'embarqué. Les étudiants y apprennent la manipulation d'un système GNU/Linux pour configurer et utiliser un réseau WiFi en mode Ad-hoc, la compilation croisée (cross-compilation) pour le développement d'applications sur systèmes embarqués, ainsi que la mise en pratique d'algorithmes de la théorie des graphes pour optimiser l'utilisation d'un réseau dont la topologie est connue. À la suite de ce module, les étudiants auront acquis des compétences rares et très recherchés sur le marché professionnel des réseaux et systèmes embarqués.

UE 9 : Programmation orientée sécurité (Olivier Levillain, Kim Nguyen)

Acquérir de bonnes pratiques de programmation pour éviter certaines failles de sécurité, découvrir les atouts et faiblesses en termes de sécurité de quelques langages de programmation.

UE 10: Programmation C++11 avancée (Joël Falcou, Guillaume Melquiond)

Ce module vise a fournir une maîtrise du langage C++ et des techniques de développement logiciel associées. L'accent sera mis sur la version moderne du langage (C++11/14) et ses implications sur les techniques de génie logiciel usuelles. Le module sera partagé entre cours théorique et manipulation sur machine.

UE 11: Modélisation et simulation de systèmes dynamiques (Alexandre Chapoutot)

L'objectif de ce cours est présenter les concepts fondamentaux de la conception dirigée par les modèles dans le cadre de la conception des systèmes de contrôle-commande. Une présentation des outils Matlab/Simulink/Stateflow permettra d'introduire les concepts de modélisation à flot de données (Simulink) et événementielle (Stateflow). Un parallèle avec l'approche synchrone sera également fait. La problématique de le couverture de modèles sera également traitée.

UE 12: Formation à la vie de l'entreprise (Nadège Taillard, Alexandre Kaminski)

La formation à la vie de l'entreprise s'articule autour des 5 thèmes suivants : gestion d'entreprise, conduite de projet, droit social,management, communication

UE 13 : Software Model Checking (Sébastien Bardin, Sylvain Conchon, Fatiha Zaïdi)

Ce cours est une introduction à la technique du model checking qui permet de vérifier automatiquement des propriétés de sûreté et de vivacité des sytèmes. Les outils de model checking sont très utilisés dans le monde industriel, en particulier dans la phase amont du développement de ces systèmes. Le cours présentera à la fois les langages de modélisation et les algorithmes sous-jacents pour vérifier des propriétés de sûreté et vivacité.

UE 14: Vérification déductive de programmes (Julien Signoles, Andrei Paskevich)

L'objectif de cette UE est de faire découvrir la spécification formelle et la vérification déductive de programmes à travers l'utilisation des outils Why3 et Frama-C.

UE 15: Systèmes réactifs et synchrones (Marc Pouzet)

Les langages synchrones permettent de programmer des systèmes réactifs embarqués à la fois très complexes et très sûrs. Ils rencontrent un grand succès dans divers domaines industriels, pour la programmation du logiciel de controle/commande dans les avions, les trains, les centrales nucléaires, etc. Le système de commande de vol des Airbus, par exemple, est développé avec l'outil SCADE issu du langage synchrone Lustre. Ils sont fondés sur le modèle du parallélisme synchrone qui introduit une notion de temps logique dans les programmes et donne la possibilité d'écrire des programmes parallèles déterministes. Le compilateur d'un langage synchrone garantit des propriétés de sûreté importantes pour le logiciel critique: exécution déterministe du code, absence de blocage (deadlock), génération de code séquentiel s'exécutant en temps et mémoire bornés, génération de code parallèle, etc. Le cours donne une introduction au modèle synchrone et à quelques langages qui en sont issus. Il présente leurs fondements mathématiques, les techniques de compilation vers du logiciel et des circuits, leur vérification formelle (par model-checking) et certains travaux de recherche récents. Nous consacrerons la fin du cours aux travaux actuels sur la sémantique et l'implémentation des langages de modélisation des systèmes hybrides combinant temps discret et temps continu, tels que Simulink/Stateflow et Modelica.

UE 16: Validation inductive de programmes et de systèmes hybrides (Sylvie Putot)

L'analyse statique de programmes consiste à vérifier statiquement (i.e. sans les exécuter) des propriétés dynamiques (à l'exécution) des programmes. Les classes de propriétés à vérifier sont très diverses comme la sûreté (par exemple l’absence d'erreurs à l'exécution), la vivacité (par exemple la garantie de réponse à un signal donné), la sécurité (par exemple la confidentialité d'informations traitées par un programme), etc. La grande difficulté pour démontrer automatiquement ces propriétés dynamiques réside dans le fait de trouver les bons arguments inductifs nécessaires pour en faire la preuve. Diverses solutions sont possibles : le demander à l'utilisateur (méthodes déductives), se restreindre à un modèle fini (vérification exhaustive) ou calculer l'argument inductif par approximation de la sémantique du programme (via des techniques d'approximation de point fixe de l'interprétation abstraite). Le cours explore cette dernière technique. La validation des systèmes embarqués critiques en constitue une application naturelle. Une difficulté qui apparait rapidement dans ce cadre est la nécessité de prendre en compte l'interaction du système avec son environnement physique. Les systèmes à valider sont alors hybrides, c'est-à-dire couplent des composantes discrètes et continues. Nous concluerons le cours par une ouverture sur la modélisation et l'analyse de tels systèmes.

UE 17: Test de conformité (Pascale Le Gall)

Les systèmes informatiques deviennent aujourd'hui complexes, distribués, embarqués et leur conception intègre des contraintes fortes tant en ce qui concerne les données que le temps. Aussi, leur test est crucial pour leur mise en production et leur maintenance. Parmi les techniques de test, les approches basées sur les méthodes formelles, aussi appelées test de conformité, visent à la génération automatique de séquences de données de test au regard de critères de sélection, de harnais de, de scripts de test, d'analyse des sorties.

UE 18: Algorithmique répartie (Sylvie Delaët, Janna Burman)

Le principal objectif d'appréhender les concepts de l'algorithmique réparti. Pour permettre à chacun de comprendre l'intérêt et les problèmes rencontrés pour l'étude et la conception d'algorithmes répartis. Un effort particulier sera demandé sur la spécification des problèmes, la formalisation des preuves et le défi intellectuel que représente le fait de concevoir soit même des algorithmes répartis.

UE 19: Optimisation Stochastique (Abdel Lisser)

Présenter les problèmes d’optimisation où les décisions sont prises en présence d’incertitude. Il s’agit de problèmes où l’ensemble ou un sous-ensemble des paramètres est représenté par des variables aléatoires qui suivent des lois de probabilités connues à l’avance. Le cours est basé sur les fondements théoriques de l’optimisation stochastique, les différentes modélisations de l’aléa et du risque et les méthodes de résolution associées. Un intérêt particulier est donné aux problèmes combinatoires stochastiques, i.e., des problèmes d’optimisation stochastiques en présence de variables entières.

UE 20: Modèles de la nature (Joffroy Beauquier, Janna Burman)

Récemment ont été introduits deux modèles directement reliés à certains comportements observables dans la nature, les algorithmes naturels et les protocoles de populations. Les algorithmes naturels constituent un langage très expressif pour modéliser les systèmes biologiques ou sociologiques et les phénomènes de synchronisation et de coordination que l'on peut observer au sein de ces systèmes multi-agents. Cette expression algorithmique permet non seulement d'effectuer des simulations numériques mais aussi et surtout fournit un cadre puissant pour l'analyse de ces systèmes. Pour les sciences du vivant, les algorithmes naturels jouent ainsi un rôle analogue à celui des équations différentielles en Physique ; il devient alors nécessaire de développer un calcul algorithmique qui serait aux sciences du vivant ce que le calcul différentiel est à la Physique. Parallèlement ont été introduits les protocoles de populations, le terme impliquant une relation avec les populations animales. Il s'agit aussi d'un modèle d'agents communicants, avec des hypothèses minimales, dans lequel des agents fixes ou mobiles, anonymes et indistinguables, avec des ressources très faibles, communiquent de manière asynchrone et imprévisible. Étudiés initialement comme modèle de calcul, les protocoles de populations ont ensuite été enrichis pour fournir des solutions à des problèmes répartis classiques. Eux aussi, mais de manière différente, permettent d'étudier des phénomènes de synchronisation et de coordination entre agents. L'objectif de ce thème est d'abord de mettre en relation deux approches menées dans des communautés différentes, de donner une vue complète de l'état de l'art dans les deux modèles, de décrire les problèmes ouverts, qui sont nombreux et de définir des perspectives de recherche qui pourraient donner par la suite naissance à un doctorat.