DOCTORANT EN METHODES FORMELLES « PREUVE FORMELLE DU RESPECT DU BESOIN POUR UNE SOLUTION DE TRANSPORT INNOVANTE » CDD 36 MOIS H/F REF VN-2018/17

Centre d’essai et de recherche appliquée de la filière ferroviaire, l’IRT Railenium (http://railenium.eu/fr/) a pour mission de développer par l’innovation collaborative la compétitivité des entreprises comme moteur de croissance et d’emplois. Railenium met en œuvre des partenariats d’innovation entre les industriels (au sens large : gestionnaires d’infrastructures, opérateurs, constructeurs et ingénieries) et le milieu académique pour assurer une réponse de haut niveau aux enjeux de la filière ferroviaire.

 

Basé dans les Hauts-de-France, soutenu par l’État et la filière ferroviaire, et agissant en synergie avec le pôle de compétitivité i-Trans sur les transports terrestres, l’IRT est adossé à un réseau d’excellence de centres et laboratoires de recherche.

L’un des trois programmes de R&D et d’innovation de Railenium vise notamment à apporter les outils et briques technologiques nécessaires au développement du Train Autonome. De par une approche système pour l’exploitation de ces trains autonomes, ce programme « Train Autonome » adressera ainsi les nouveaux systèmes de signalisation, de contrôle-commande, de conduite et d’exploitation ferroviaire. Pour mener à bien ses projets, le programme Train Autonome est à la recherche d’un doctorant en méthodes formelles.

 

Dans le cadre du programme Train Autonome, l’un des objectifs est de proposer une méthodologie outillée pour prouver formellement la conformité d’une spécification industrielle avec une expression du besoin, effectuée en amont. Ce besoin sera formalisé en utilisant une approche formelle orientée but. En effet, les méthodes formelles sont pleinement recommandées par les normes européennes.

 

Dans une première étape, le travail s’appuiera sur une ontologie qui va définir un ensemble structuré des termes et de concepts métiers. Sur la base de cette ontologie, différents services alignés sur les buts seront affectés à un certain nombre de rôles, dans le cadre d’un formalisme orienté rôle. A partir de ce modèle exprimé dans un profil UML, l’outil B4M secure pourra être utilisé afin de produire un modèle formel sur lequel les propriétés spécifiées seront vérifiées.

 

Dans une deuxième étape, une proposition industrielle sera analysée et nous relierons les éléments d’architectures aux grands concepts du domaine en se basant sur une ontologie du domaine ferroviaire.

 

La dernière étape de ce travail de thèse devra s’appuyer sur les travaux scientifiques concernant l’alignement d’ontologies pour établir des liens sémantiques entre le modèle du besoin et la spécification proposée [10]. Ces liens sémantiques devraient permettre de prouver formellement la conformité de la spécification avec l’expression du besoin, par exemple en produisant un modèle formel de la spécification et en caractérisant formellement ses relations avec le modèle du besoin défini dans la première étape.

 

De manière plus globale, la première phase de cette thèse sera consacrée à une étude de la bibliographie scientifique et à une acquisition des connaissances ferroviaires nécessaires à la bonne compréhension des enjeux du projet (6 mois). A l’issu de ce travail, le doctorant prendra un an pour construire des propositions méthodologiques, dont le fond scientifique sera validé dans une conférence scientifique du domaine (FORTE, ABZ, Formalize, FMiCS ou MEDI par exemple) et dont la validité applicative sera attestée par une publication dans une conférence ferroviaire (Comprail, Safe ou RSSRail). Ces propositions seront validées par un outillage formel et seront  soumises à une revue de référence (SoSyM, JUCS, SIC, IJCCC). Enfin, l’illustration sur un cas d’étude inspiré du train autonome devra convaincre la communauté ferroviaire (revue Transportation Research). La dernière phase de la thèse finalisera le mémoire de doctorat.

 

Vous êtes titulaire d’un Master/Ingénieur informatique avec un cursus en Génie Logiciel,

Vous avez des connaissances sur la modélisation UML, les méthodes formels ou encore sur le développement d’outils Logiciels (Java) avec une bonne logique Mathématique,

L’autonomie et le sens de l’initiative ne vous font pas peur,

Vous appréciez travailler en équipe et avez un bon relationnel,

La créativité et l’organisation sont des qualités que l’on vous a reconnues,

Vous avez une excellente capacité rédactionnelle et parlez couramment Français avec une aisance en anglais

 

n’hésitez pas à postuler : https://railenium.eu/?post_type=job

 

Travail en collaboration avec le laboratoire ESTAS de l’Ifsttar (www.estas.ifsttar.fr/).

 

CDD 36 mois basé sur Villeneuve D’Ascq