Science du logiciel

Si on regarde l'histoire des langages de programmation, on s'aperçoit que la plupart des langages (ou concepts) de programmation utilisés aujourd'hui n'existaient pas il y a vingt ans. Aussi, il est tout à fait légitime de se demander comment seront programmer les applications de demain.

Si on regarde l'histoire du développement logiciel, on s'aperçoit que la taille des logiciels développés aujourd'hui est sans commune mesure avec les logiciels d'hier. La plupart des logiciels industriels sont tellement gros (en nombre de lignes de code) qu'il n'existe pas un programmeur qui le comprenne dans sa totalité. Le développement est donc un travail d'équipe! Aussi, il est tout à fait légitime de se demander comment faire comprendre à l'autre ce qu'un module d'un logiciel est censé faire.

Si on regarde l'histoire de l'industrie du logiciel, on s'aperçoit que la pression du marché impose que les délais pour produire un logiciel se raccourcissent. Aussi, il est tout à fait légitime de se demander comment programmer sans introduire trop de bugs dans de telles conditions.

Le profil Science du Logiciel tente d'apporter des réponses à toutes ces questions. En particulier, l'accent sera mis sur les techniques de programmation avancées, les langages de programmation modernes et les outils utilisés aujourd'hui pour découvrir les bugs ou garantir leur absence.

Emploi du temps

L'emploi du temps pour le parcours Science du Logiciel est accessible ici

Projets tutorés

Liste des UE (toutes à 2.5 ECTS)

Programmation d'applications Web avancées (Cours:10.5h, TD:10.5h)
Intervenants : Kim Nguyen (UPsud), Fatiha Zaïdi (UPsud)
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).

Programmation systèmes et réseaux (Cours:10.5h, TD:10.5h)
Intervenant : Steven Martin (UPsud)
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.

Programmation orientée sécurité (Cours:10.5h, TD:10.5h)
Intervenants : Olivier Levillain (ANSSI), Kim Nguyen (UPsud)
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.

Pour vous faire une idée: Deux articles intéressants de l'ANSSI (Agence Nationale de la Sécurité des Systèmes d'Information) sur les liens entre langage de programmation et sécurité: Sur Java et sur les langages de programmation fonctionnels

Programmation C++11 avancée (Cours:9h, TD:6h, TP:6h)
Intervenants : Joël Falcou (UPsud), Guillaume Melquiond (INRIA)
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.

Langages centrés données (Cours:10.5h, TD:10.5h)
Intervenants: Véronique Benzaken (UPsud), Kim Nguyen (UPsud)
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.

Outils de test, critères et stratégies de couverture (Cours:10.5h, TD:10.5h)
Intervenants: Christophe Gaston (CEA), Nikolay Kosmatov (CEA), Delphine Longuet (PSud), Fatiha Zaïdi (PSud)
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.

Test de conformité (Cours:21h)
Intervenants: Pascale Le Gall (ECP), Stéphane Maag (TSP), Burkhart Wolff (UPsud)
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.

Software Model Checking (Cours:10.5h, TD:10.5h)
Intervenants: Sébastien Bardin (CEA), Sylvain Conchon (UPsud), Fatiha Zaïdi (UPsud)
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é.

Vérification déductive de programmes (Cours:10.5h, TP:10.5h)
Intervenants: Julien Signoles (CEA), Andrei Paskevich (UPsud)
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.

Modélisation et simulation de systèmes dynamiques (Cours:7h, TP:14h))
Intervenants: Alexandre Chapoutot (ENSTA)
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.

Validation inductive de programmes et de systèmes hybrides (Cours:10.5h, TD:10.5h)
Intervenants: Sylvie Putot (École Polytechnique)
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.

Vérification/Preuves interactives et applications (Cours:9h, TP:12h)
Intervenants: Burkhart Wolff (UPSud), Christine Paulin (UPsud)
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 de deux systèmes majeurs : Coq et 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.

Page du cours.