~ Curriculum VITAE ~

    Cortier Alexandre
    Docteur-Ingénieur en Informatique
    Né le 02/03/1981 à Juvisy s/Orge (91)
    Spécialités : Modélisation et Méta-Modélisation, Génie Logiciel, IDM (Ingénierie Dirigée par les Modèles), Méthodes Formelles, Systèmes Embarqués et Temps-Réel, Interaction Homme-Machine (IHM)
Parcours Professionnel
2008-...


Post-Doctorat en Informatique depuis le 15 Juin 2008 à l' IRIT au sein de l'équipe ACADIE (Assistance à la Certification d'Applications DIstribuées et Embarquées). Bourse INPT du 15 au 31 Octobre. Bourse CNES depuis le 1er Novembre, Projet SPaCIFY.
2004-2008

Doctorat en Informatique à l' ONERA au sein du DTIM (Département Traitement de l'Information et Modélisation). Projet VERBATIM.
2004-2007
Vacataire d'Enseignements à Toulouse (SUPAERO, INSA, ENSA) (Voir page enseignements).
2004
(6 mois)
Projet de Fin d'étude (PFE) au LISI / ENSMA (Poitiers) dans l'équipe Ingénierie des données.
2003
(4 mois)
Stage Ingénieur au CSTB (Centre Scientifique et Technique du Bâtiment, Marne-la-Vallée, 77).
Formation / Diplômes
2008






Doctorat (Spécialité informatique) (ONERA-DTIM - Université de Toulouse, Supaero, France). Sujet : Validation formelle de Systèmes Interactifs par analyse statique de code source Java/Swing. Soutenu le 6 Juin 2008. Jury :
Présidente du Jury : Laurence Nigay (Pr., LIG, Grenoble)
Directeur de thèse : Bruno d'Ausbourg (IR,ONERA-DTIM, Toulouse)
Rapporteurs : Christophe Kolski (Pr., LAMIH, Valenciennes), Ioannis Parissis (MdC, LIG, Grenoble)
Examinateurs : Yamine Aït-Ameur (Pr., LISI-ENSMA, Poitiers), Dominique Méry (Pr., LORIA, Nancy)
2004

Diplôme d'Ingénieur ENSMA, (Ecole Nationale Supérieure de Mécanique et d'Aérotechnique - Poitiers).
2004


DEA d'Informatique (Université de Poitiers), T3ia : Traitement de l'Information, Informatique, Image et Automatique. Mention Bien.
2003

Maîtrise de Mécanique des Solides (Université de Poitiers), Mention Bien.
2001-2002
Classes Préparatoires aux Grandes Ecoles - MPSI au Lycée Hoche (Versailles) et PSI* au Lycée J-B. Say (Paris)
1999
Baccalauréat scientifique, option mathématique - Lycée François Truffaut (Bondoufle,91), Mention Bien.
Activités détaillées

Post-Doctorat (IRIT)

2008

-

...

 

 

 

 

 

 
Post-Doctorat : Projet SPaCIFY.

Mission :

 Post-Doctorant CNES au sein de l'équipe ACADIE (Assistance à la Certification d'Applications DIstribuées et Embarquées) à l'IRIT dans le cadre du projet ANR SPaCIFY.

Dates :
Novembre 2008 - Novembre 2010

Actions :

Animateur du projet SPaCIFY au sein de l'équipe ACADIE.
Organisation et animation de réunions de travail autour du projet SPaCIFY.
Travail en collaboration avec les partenaires industriels (EADS Astrium, Thales Alenia Space, ONERA, Anyware Technlogy) et académiques (IRISA-ESPRESSO, Telecom Bretagne, Labri).
Définition du langage métier Synoptic dédié à la conception de systèmes embarqués pour l'aérospatial : définition de la syntaxe abstraite (méta-modèle Ecore), syntaxe concrète (TCS : Textual Concrete Syntax)
Définition et programmation de règles OCL (règles structurelles du langage Synoptic).
Définition de la sémantique formelle du langage Synoptic (sémantique synchrone).
Réalisation d'étude de cas en collaboration avec le CNES (Système de Contrôle d'Attitude et d'Orbite).

Responsable:
Mamoun Filali (Chargé de Recherche CNRS)

Résumé:
Mes travaux de post-doctorat s'inscrivent dans le projet ANR Spacify. L'objectif du projet, réunissant de nombreux partenaires industriels et universitaires, est de définir une méthodologie de conception et de validation de systèmes embarqués pour le domaine aérospatial. Cette méthodologie, orientée Ingénierie des Modèles (IDM) doit être concrétisée par un outil sous la plate-forme TOPCASED (conception de modèles graphiques, transformations assistées, vérification \& simulation, génération de code). Je participe à la définition d'un langage de spécification métier (Synoptic) devant servir de support au projet. La définition du langage regroupe les définitions de la syntaxe abstraite (méta-modélisation Ecore), de la syntaxe concrète et de la sémantique du langage (synchrone multi-horloge). Une fois le langage stabilisé et sa sémantique formelle définie, mes travaux se porteront sur la validation de transformations, le but étant d'assister le concepteur en lui offrant un panel de transformations sûres. Les transformations à vérifier, liées aux pratiques industriels dans la dynamique du processus de développement, sont de plusieurs types : raffinements, transformations d'édition, transformations métiers... L'objectif est d'utiliser un cadre formel tel la méthode B ou un assistant de preuve tel que ou Coq afin de vérifier ces transformations.

Communications :

Conférences, Workshops, Posters... (cf. publications)
1 Chapitre de Livre (cf. publications)
Rapports Internes de Recherche

Thèse (ONERA)

2004

-

2008


















Validation formelle de systèmes Interactifs par analyse statique de code source Java/Swing

Mission :
Doctorant au sein du DTIM (Département Traitement de l'Information et Modélisation) à l'ONERA dans le cadre du projet VERBATIM.

Action :

Développement d'une méthodologie de validation formelle de systèmes interactifs Java/Swing vis à vis de spécification sous forme de modèles de tâches (CTT). L'approche consiste à extraire d'une application Java-Swing un modèle comportemental capturant l'évolution des dispoinibilités d'interaction de l'interface (modèle formel du dialogue de l'application ). Cette extraction exploite les techniques d'analyses statiques et d'abstraction de programmes. Les langages B événementiel et NuSMV ont été utilisé pour la description des modèles extrait et la validation de l'application.

Bibliographie :
Cycle de développement IHM, génie logiciel, modèles de tâches, modèles utilisateur, modèles de description de dialogue, annotations de code source JML, test, validation et vérification, logiques temporelles (LTL,CTL), méthodes formelles, systèmes de preuves (Theorem Proving, Model-Checking);

Outils :

 Développement --> Eclipse, Emacs (Développement), JavaCC, JJTree, CTTE ;
Méthodes formelles --> méthode B et B événementielle (plate-forme Rodin, Click'n'Prove et B4free, Atelier B), méthode NuSMV ;
Analyse Statique --> Javacc/JJTree, reconnaissance de pattern, abstraction, modèles intermédiaires (AST,CFG);

Communications :

Conférences (1 article international publié, 1 article national publié), 5 articles non édités (Workshops);

PFE
&
DEA
(LISI)

2004









(Méta)-Modélisation d'une architecture à base de composant pour l'avionique : Utilisation du langage de modélisation EXPRESS.

Action :

(Méta)-Modélisation d'une architecture à bases de composants pour la conception de systèmes avioniques dans le cadre de l'AMI (Architecture Modulaire Intégrée). Implémenation du méta-modèle (EXPRESS,ECCHO) permettant la composition de composants de manière opérationnelle. Représentation des composants multi-couche (Matériel, Logiciel, Connectivité). Architecture basée sur la Théorie des Catégories pour spécifier formellement la notion de composition des différents composants (Pushout). Aperçu des réseaux ARINC et AFDX ;

Outils :

 EXPRESS (équivalent UML+OCL) et son environnement ECCHO. ECCHO permet l'instantiation d'un méta-modèle EXPRESS.

Communications :

1 article international avec actes édités, 1 article national (worshop); Rédaction d'un mémoire.

 
Stage
Ingénieur
(CSTB)

2003



Analyse statistique du comportement en traction et cisaillement de chevilles pour béton.

Action :

Analyse statistique du comportement en traction et cisaillement de chevilles pour bétons à partir d'une base de données d'essais existante. Comparaison des résultats d'essai avec les modèles physique existants. Proposition de nouveaux modèles de comportement suivant le type de chevilles (modèle, dimensions) et le type de béton.

Outils :

 Utilisation d'EXCELL (développement de macro)
Compétences
Mes principales connaissances concernent la modélisation des systèmes et le traitement de l’information.

 Plus particulièrement, je dispose de bases solides concernant l’utilisation des méthodes formelles. Les méthodes formelles sont principalement utiles pour le développement et la validation de systèmes dits « critiques » (aéronautique, nucléaire, automobiles). L’utilisation de ces méthodes permet de s’assurer de la fiabilité des systèmes conçus (propriétés de sûreté, d’équité,…).  Si l’utilisation de ces méthodes ne peut suppléer l’utilisation classique du test, elle peut néanmoins permettre d’en réduire le nombre. Lustre (Scade) est une méthode formelle particulièrement utilisée par Airbus pour la conception des systèmes de commandes. L’entreprise Clearsy exploite quant à elle la méthode formelle B dans le domaine des transports ferroviaire. Pour conclure, notons que les méthodes formelles sont particulièrement exploitables dans le domaine de la sûreté de fonctionnement.

Concernant la programmation, trois années de thèse m’ont permis d’acquérir une certaine aisance pour la majorité des  langages de programmation existants. Je dispose également de bases solides concernant la programmation temps réel. Je dispose également de quelques connaissances concernant l’architecture des systèmes avioniques (AMI : Architecture Modulaire Intégré).
OS
Windows, Linux, Unix, Solaris
Langages
  1. Langages de programmation :
    1. Généraux : Java, C, C++, Ada, Fortran, MathLab, LabView
    2. Temps Réel : Ada temps réel, C (VxWorks), Lustre, Scade,
    3. Web : HTML, PHP, XML, JavaScript
    4. Base de données : SQL
  2. Langages de modélisation :
    1. UML, EXPRESS, Ecore
    2. StateCharts, Lustre (Scade), Esterel,
  3. Langage de description : SART, SADT
Langages
Formels
  1. Theorem Proving: B et B événementiel
  2. Model Checking: Promela, NuSMV, Lustre, UPPAAL (automates temporisés)
  3. Logiques Temporelles: LTL, CTL
  4. Formalismes : Automates, Réseaux de Petri
Outils
Logiciels
  1. Développements : Emacs, Eclipse, Tornado, Dreamweaver
  2. Méthodes Formelles: Atelier B, B4free, Rodin, NuSMV, Bandera
Analyse
Statique
  1. Parser : JavaCC, JJTree et LeX et Yacc (connaissances)
  2. Représentation abstraites : grammaires, AST, CFG (Control Flow Graph), SDG (Système DependanceGraph)
Temps Réel
  1. Noyau temps réel : VxWorks
  2. Connaissances des différentes politiques d’ordonnancement et des différents mécanismes de communications multi-tâches.
  3. Langages : Ada, C
  4. Programmation synchrone : Scade, Lustre, Esterel, Signal
Langues
  1. Anglais courant (TOEIC : 735)
  2. Allemand : connaissances scolaires
Expériences personnelles et Charges collectives
2008
Organisation et animation de réunions
    Animation d'une réunion plenière à l'IRIT-Toulouse dans le cadre du projet ANR Spacify (15-16 Septembre). Participants industriels : CNES, Alcatel Alenia Space (Thales), EADS Astrium, Anyware Technologie,GEENSYS, ONERA-DTIM Toulouse. Participants universitaires : ENSTB (équipe CAMA), IRISA (équipe ESPRESSO), IRIT (équipe ACADIE), LABRI.
    Réunion ``Outils Graphiques pour Synoptic : intégration à la plateforme Topcased''. ACADIE/Anyware Technologies (17 Nov. 2008).
    Réunion ``Transformations métiers''.ACADIE/Alcatel Aliena Space (5 Nov. 2008).
    Réunion ``Développement du langage Synoptic : retours''. ACADIE/Astrium (15 Oct. 2008).
2005-2006
Participation à l'organisation de la journées des Thèses de l'ONERA.
2001-2004

Membre du bureau des élèves (BdE) de l’ENSMA.
Président du Club Escalade de l’ENSMA .
2002
(1 mois)
Stage ouvrier chez Spie Trindel. Site d'assemblage d'Airbus à Saint-Nazaire (44)
2001
(1 mois)
Intérimaire chez Alcatel sur le site de Vélizy-Villacoublay (78). Service comptabilité.
2000
(2 mois)
Saisonnier au centre VVF de Soustons (40). Animateur enfants/adulte.
1995-1998
Moniteur de Gymnastique Agrès. Club FSCF de  Bondoufle (91), 1 degré d’encadrement (Poussin)
Divers
  1. Titulaire du permis B
  2. Loisirs :
    1. Sports : Escalade, Alpinisme, Randonnée, Gymnastique, Course à pied.
    1. Musique : Guitare, didgeridoo.
    2. Autres : Lecture, écriture

     
Enseignements
2004 - 2005 : Supaero (Toulouse), INSA (Toulouse), ENSA (Marrakech)

Type

Cours

Section

Heures/TD

Cours

Programmation Réactive et Méthodes Formelles

Master 2 - CAMSI
5ème-INSA
(TRS)

60h

TP

Technologie Objet et programmation Java

1ère- ENSEEIHT

25h

TP

Outils pour le génie logiciel

1ère- ENSEEIHT

16h

TP

Programmation Temps-Réel

4ème-INSA(TR)

18h

TD - TP

Programmation réactive

Master 2 - CAMSI
5ème- INSA (TRS)

5ème- ENSA

98h

TP

Langage Lustre

3ème - SUPAERO

12,5h

Volume horaire (équivalent TD)

219,5h
Télécharger mon CV

Attention : Pour visualiser les documents, votre navigateur doit disposer du plugin d'Acrobat Reader. Si vous ne parvenez pas à télécharger les documents : utiliser le click droit de la souris sur l'icône et choisissez "Save Link Target As".

 

 

CV long (pdf)

CV - Dossier de candidature aux fonctions de Maître de Conférence (pdf)