Curriculum Vitæ Marion GUTHMULLER ´ Universit´e de Lorraine / LORIA - Equipe AlGorille [email protected] N´ee en Mai 1988 Nationalit´e Fran¸caise Parcours Depuis Oct. 2011 ´ Doctorat en Informatique - Universit´e de Lorraine / Equipe de recherche AlGorille, LORIA (laboratoire LOrrain de Recherche en Informatique et ses Applications) et Inria Nancy Grand-Est 2010 – 2011 Master 2 Informatique, parcours Recherche, sp´ ecialit´ e SSR (S´ ecurit´ e, Services et R´ eseaux) - Mention Assez Bien - Universit´e de Lorraine 2008 – 2011 Diplˆ ome d’Ing´ enieur en informatique, approfondissement IL (Ing´ enierie du Logiciel) - ESIAL (nouvellement TELECOM Nancy), Universit´e de Lorraine 2006 – 2008 D.U.T. Informatique - IUT Charlemagne, Universit´e de Lorraine 2006 Baccalaur´ eat s´ erie S, option SVT, sp´ ecialit´ e Math´ ematiques - Mention Bien Lyc´ee J.A. Margueritte, Verdun (55) Exp´ erience professionnelle Oct. 2011 – Sept. 2014 Doctorante contractuelle, `a l’Universit´e de Lorraine, Nancy, France ´ Equipe de recherche : AlGorille (LORIA et Inria Nancy Grand-Est) ´ Travaux de recherche : Etude et v´erification des applications distribu´ees R´esum´e : Mon travail porte sur l’´etude conjointe de la performance et de la correction des applications distribu´ees. Pour cela, nous nous appuyons sur l’outil de simulation SimGrid qui permet l’´etude d’applications `a large ´echelle telles que les grilles, le calcul haute performance, le pair-`a-pair ou bien le Cloud. Au sein de cette outil est d´evelopp´e l’outil de v´erification SimGridMC qui permet la v´erification dynamique (en ex´ecutant et en v´erifiant l’application r´eelle) des applications ´etudi´ees `a travers le simulateur. L’objectif de mes travaux est de permettre la v´erification des propri´et´es de vivacit´e et la d´ecouverte automatique de propri´et´es d’ex´ecution dans les sch´emas de communication des applications MPI. Directeurs : Martin Quinson et Sylvain Contassot-Vivier Enseignement : niveau L1, L3 et M1 `a l’UFR Math´ematiques et Informatique Depuis 2005 Cours particuliers et aide aux devoirs Mati` eres : Math´ematiques, Fran¸cais, Informatique, Physique-Chimie Je dispense des cours particuliers individuels de niveau coll`ege `a lyc´ee `a des ´etudiants dont le nombre et le niveau ´evoluent au cours des ann´ees, `a raison de une `a quatre heures par semaine par ´etudiant. J’ai suivi certains d’entre eux sur plusieurs ann´ees (2 `a 3 ans) ce qui me permet de travailler sur du long terme et de voir ´evoluer les ´etudiants en m’adaptant ` a leurs besoins. Selon les s´eances, soit il s’agit d’aide aux devoirs ou de la pr´eparation aux examens, ou bien ce sont des cours suppl´ementaires. Ceci me permet de compl´eter mes comp´etences en enseignement acquises lors de mon monitorat, avec en particulier une approche individuelle qui n’est pas toujours possible dans l’enseignement a l’Universit´e. Je suis donc capable de cibler plus facilement les difficult´es de chacun ` pour proposer une d´emarche personnalis´ee. Appliqu´ee au monde universitaire, ceci me permet d’avoir une meilleure approche avec les ´etudiants et surtout de d´etecter plus facilement/rapidement des ´eventuels ´etudiants en difficult´e. 1 sur 6 F´ev. 2011 – Sept. 2011 Stage de Master 2 Recherche / 3`eme ann´ ee ESIAL, au sein de l’´equipe AlGorille (LORIA et Inria Nancy Grand-Est), Nancy, France Sujet : Stateful model checking et v´erification de propri´et´es de vivacit´e dans SimGrid R´esum´e : le model checking d´esigne une technique de v´erification automatique des syst`emes dynamiques o` u il s’agit de d´eterminer grˆace `a un algorithme si un mod`ele d’un syst`eme donn´e satisfait certaines propri´et´es. L’outil de simulation SimGrid impl´emente un model checker permettant la v´erification dynamique de propri´et´es de sˆ uret´e directement ` a partir d’un code C. L’objectif de ce stage ´etait d’ajouter la v´erification de propri´et´es de vivacit´e, formul´ees en termes de Logique Temporelle Lin´eaire (LTL). Une ´etude sur la limitation de l’explosion combinatoire de l’espace d’´etat a ´egalement ´et´e r´ealis´ee en se basant sur une technique de r´eduction dynamique par ordre-partiel d´ej` a utilis´ee pour les propri´et´es de sˆ uret´e. Technologies : C et Lex/Yacc Sept. 2010 – Mars 2011 Projet industriel de 3`eme ann´ ee ESIAL, au FMI (Fonds Mon´etaire International), ´ Washington DC, Etats-Unis ´ Sujet : Etude et d´eveloppement d’outils de g´eo-visualisation R´esum´e : l’objectif de ce projet ´etait de d´evelopper un outil de g´eo-visualisation permettant de repr´esenter sur une carte les donn´ees mondiales du FMI pour divers indicateurs. Une premi`ere phase d’´etude des outils existants a permis de d´eterminer l’outil le plus adapt´e aux besoins et exigences du FMI, puis un prototype bas´e sur ce dernier a ´et´e d´evelopp´e. Celui-ci permet de r´ecup´erer automatiquement les donn´ees sur le serveur REST du FMI et de les visualiser selon diff´erentes repr´esentations. Diverses options permettent de mettre en avant certaines caract´eristiques ou d’automatiser la visualisation sur une p´eriode donn´ee. Technologies : HTML 5, CSS, Javascript et JQuery Juin 2010 – Sept. 2010 Stage de 2`eme ann´ ee ESIAL, au sein de l’´equipe AlGorille (LORIA et Inria Nancy Grand-Est), Nancy, France Sujet : Interception syst`eme pour la capture et le rejeu de traces R´esum´e : au sein du projet SimGrid, le projet Simterpose vise `a permettre l’´etude sur simulateur d’applications compl`etes dans le but de les ´emuler. Pour cela, il est n´ecessaire d’intercepter les actions de ces applications ayant un impact sur leur environnement. Une ´etude des diff´erents moyens d’interception a ´et´e r´ealis´ee puis, un prototype bas´e sur l’appel syst`eme ptrace a ´et´e impl´ement´e dans le but de l’int´egrer `a l’outil de simulation SimGrid. Technologies : C, programmation Syst`eme et R´eseau sous Linux Janv. 2010 – Mai 2010 Projet d’Initiation et de D´ ecouverte ` a la Recherche, au CRAN (Centre de Recherche en Automatique de Nancy) en partenariat avec l’Or´eal Paris, France Sujet confidentiel sur le Traitement Num´erique d’Images. Technologies : Matlab D´ec. 2008 – Juin 2009 Webmaster, pour l’entreprise F.B.M. S.a.r.l, Nancy, France Technologies : PHP et CSS Juin 2008 – Aoˆ ut 2008 Stage de fin d’´ etudes D.U.T. Informatique, dans l’entreprise SEPAREX, Champigneulles, France Sujet : Restructuration et d´eveloppement du site Internet de l’entreprise SEPAREX Technologies : PHP, MySQL, Flash et Javascript 2 sur 6 Comp´ etences informatiques Programmation C, Langages de scripts (Bash et Perl), environnement multi-thread, programmation syst`eme Linux, Java, J2EE, Cobol, Matlab, XML/XSL, structures de donn´ees Syst`emes GNU/Linux (Debian, Ubuntu) et Windows R´eseaux Programmation r´eseau (C et Java), routage, protocoles internet, analyse avec Wireshark Base de donn´ees Mod`ele relationnel/mod`ele EA, SQL, MySQL, Oracle, JDBC Web Standards du W3C, (X)HTML(5), PHP, CSS, JavaScript, JSP et Framework JSF Conception M´ethode Merise, notation UML Conduite de projets Planification des coˆ uts, diagrammes de GANTT, PERT Gestion de versions Git, SVN IDE Eclipse et Netbeans Divers LATEX (Beamer, TikZ), Gimp, notions de programmation en Flash et JQuery, Lex/Yacc Langues Fran¸ cais Langue maternelle Anglais Courant et scientifique Espagnol Scolaire 3 sur 6 Activit´ es d’enseignement R´ ecapitulatif L’ensemble de ces enseignements a ´et´e effectu´e `a l’UFR Math´ematiques et Informatique de l’Universit´e de Lorraine, dans le cadre de mon contrat doctoral (64 HETD par an sur trois ans). J’ai ´et´e responsable (construction des CM, des TD/TP et ´ eventuels projets, r´ edaction du sujet d’examen et correction des copies) de chaque module dont le volume horaire inclus des CM. Ann´ ee Scolaire 2013 – 2014 2012 – 2013 2011 – 2012 Public Intitul´ e du module Volume (HETD) L1 MIASHS Architecture des Ordinateurs 15h CM et 10h TD L3 MIAGE Syst`eme d’exploitation et Langages de scripts (Unix, Bash et Perl) 12h CM et 24h TD/TP M1 MIAGE R´eseau 30h CM et 20h TD/TP L1 Droit Pr´eparation au C2i, Partie 1 20h TD/TP M1 MIAGE R´eseau 30h CM et 20h TD/TP L1 AES Pr´eparation au C2i, Partie 1 18h TD/TP D´ etails Architecture des Ordinateurs. L’objectif de ce cours ´etait de faire d´ecouvrir aux ´etudiants de L1 MIASHS (Math´ematiques et Informatique Appliqu´ees aux Sciences Humaines et Sociales) les principes de bases qui r´egissent l’ensemble des architectures des ordinateurs existantes (architecture de Von Neumann, d´ecomposition en couches du niveau mat´eriel jusqu’` a la programmation haut-niveau, circuits logiques et langage d’assemblage). Le volume horaire ´etant assez restreint au vu des aspects qui peuvent ´etre ´etudi´es, ce cours reste th´eorique (pas de travail sur machine). Du fait du renouvellement de l’organisation de la licence juste avant l’ann´ee d’enseignement, j’ai construit les ressources associ´ees dans leur int´egralit´e. Syst` eme d’exploitation et Langages de scripts. Ce module destin´e aux ´etudiants de L3 MIAGE (M´ethodes Informatiques Appliqu´ees ` a la Gestion des Entreprises) est d´ecompos´e en deux parties. La premi`ere, assur´ee par Christine Bourjot, porte sur les concepts de base communs `a l’ensemble des syst`emes. J’ai donc assur´e la seconde partie, dans laquelle je pr´esente aux ´etudiants le syst`eme UNIX avec une partie th´eorique de 8h de CM suivie ensuite de 24h de TD/TP. Durant ces s´eances, nous abordons dans un premier temps les concepts li´es `a UNIX tels que le syst`eme de fichiers, les processus, les droits avec les notions d’utilisateurs et groupes. Puis deux langages de scripts sont ´etudi´es en parall`ele : Bash et Perl. En plus d’un examen final ´ecrit, les ´etudiants avait un projet `a r´ealiser en binˆ ome, portant sur les deux langages : la cr´eation et la gestion d’une biblioth`eque num´erique en Bash et la r´ealisation d’un serveur Web en Perl. En l’absence de supports et suite `a une refonte d’une partie de la maquette de la licence juste avant l’ann´ee d’enseignement, j’ai enti`erement construit de z´ero la seconde partie du module. R´ eseau. Ce cours, dispens´e en M1 MIAGE, aborde, avec une approche bottom-up, l’organisation des r´eseaux. Un premier chapitre introduit le mod`ele hi´erarchique en couches avec la notion de protocoles. Puis chaque partie du cours correspond ` a une couche du mod`ele TCP/IP. En TD/TP sont ´etudi´es les protocoles IP, ICMP, UDP, TCP, telnet, SSH, HTTP, DNS. Les ´etudiants sont invit´es ` a installer eux-mˆemes serveurs et clients des protocoles applicatifs, et ` a ´etudier les diff´erents protocoles dans des conditions r´eelles au moyen d’un analyseur de trames. Je me suis appuy´ee en partie des supports de Pascal Fontaine, en charge du module pr´ec´edemment mais alors en d´el´egation, pour la r´ealisation des supports de cours. J’ai toutefois construit l’ensemble des TD/TP en int´egrant en plus des ann´ees pr´ec´edentes la programmation r´eseau en Java qui n’´etait vue ni en cours ni en TP. Grˆace `a cela, j’ai pu propos´e un nouveau projet ` a faire en 6 semaines, en binˆ ome dans lequel il leur est demand´e de coder un client POP3 utilisant le protocle TCP et un client TFTP utiisant le protocole UDP, sachant qu’un serveur est fourni pour chaque client `a impl´ementer. Pr´ eparation au C2i (Certificat informatique et internet), Partie 1. L’objectif est de pr´eparer les ´etudiants ` passer la Certification Informatique et Internet. Elle s’appuie sur deux types d’enseignements compl´ementaires : des a ressources p´edagogiques en ligne et des travaux pratiques encadr´es par un enseignant. Sont abord´es dans la Partie 1 : le traitement de texte, le syst`eme d’exploitation (commandes Windows) et les fichiers (organisation et archivage), Internet et la PAO (Publication Assist´ee par Ordinateur). J’ai assur´e ce module deux ann´ees de suite `a des ´etudiants ´ de niveau L1 de deux formations diff´erentes : AES (Administration Economique et Sociale) et Droit, donc un public majoritairement novice concernant les notions ´etudi´ees. 4 sur 6 Exp´ eriences d’encadrement En accord avec mes directeurs de th`ese, j’ai fait le choix de limiter les encadrements d’´etudiants au cours de ´ mes trois ann´ees de contrat doctoral. Etant chaque ann´ee responsable d’un ou plusieurs modules dans mon service d’enseignement, il devenait difficile pour moi de concilier cela avec des encadrements individuels d’´etudiants. C’est ainsi que j’ai encadr´e, lors de ma troisi`eme ann´ee de th`ese (de Janvier 2014 `a Mai 2014), deux ´etudiants de deuxi`eme ann´ee ` a TELECOM Nancy sur un sujet de PIDR (Projet d’Initiation et de D´ecouverte de la Recherche) que j’ai soumis en partenariat avec Martin Quinson. L’objectif de ce projet ´etait de cr´eer un outil de visualisation dynamique pour la v´erification d’applications distribu´ees dans SimGrid. Il s’agit donc d’un travail en lien direct avec mon sujet de th`ese ce qui m’a permis d’expliquer les concepts fondamentaux de mes travaux `a des n´eophytes du domaine. 5 sur 6 Activit´ es de recherche Publications Conf´ erences internationales avec comit´ e de lecture [1] « State equality detection for implementation-level model-checking of distributed applications », Marion Guthmuller – 18th International Symposium on Formal Methods - Doctoral Symposium (FMDS’12), Paris, France, Aoˆ ut 2012 Conf´ erences nationales avec comit´ e de lecture ´ [2] « Emulation d’applications distribu´ees sur des plates-formes virtuelles simul´ees », Marion Guthmuller, Lucas Nussbaum et Martin Quinson – Rencontres francophones du parall´elisme (RenPar’20), Saint-Malo, France, Mai 2011 Posters internationaux avec comit´ e de lecture [3] « System-level state equality detection for the dynamic verification of distributed applications », Marion Guthmuller et Martin Quinson – The European Conference on Computer Systems (EuroSys’14), Amsterdam, Pays-Bas, Avril 2014 Posters nationaux avec comit´ e de lecture [4] « V´erification d’application distribu´ees ` a travers la simulation et le model checking », Marion Guthmuller et Martin Quinson – Conf´erence en Parall´elisme, Architecture et Syst`eme (ComPAS’13), Grenoble, France, Janvier 2013 Communications sans publication - « V´erification dynamique d’applications distribu´ees avec SimGridMC » – Groupe de travail sur la V´erification (http://gt-verif.loria.fr), Paris, France, Juin 2014 - « D´etection de l’´egalit´e d’´etats pour la v´erification dynamique d’applications distribu´ees par model checking » – RGE (R´eseaux Grand Est) (http://rge.u-strasbg.fr/), Nancy, France, Juillet 2012 6 sur 6