QUI SOMMES-NOUS ?

L’activité Systèmes terrestres et aériens conçoit des systèmes, des équipements, des capteurs et des services pour le contrôle du trafic aérien civil et militaire, la défense aérienne ainsi que le combat naval et terrestre.Le site de Massy est leader dans les systèmes de commandement et de contrôle des opérations aériennes et les systèmes radars de défense aérienne.

QUI ETES-VOUS ?

Vous êtes de formation supérieure et vous recherchez une alternance de 1 à 2 ans ?

L’environnement informatique vous passionne ?

Vous possédez un bon esprit d’analyse et de synthèse ?

Vous aimez prendre des initiatives et êtes force de proposition ?

Dynamique et autonome, on vous reconnaît un bon relationnel et des capacités d'adaptation ?

Vous avez de bonnes compétences en langage de preuve ?

Vous connaissez UML et XML ?

Vous êtes intéressé(e) par les calculs de construction inductive ?

Vous connaissez les langages Coq, Isabelle, HOL ?

Vous maîtrisez l’extraction de programme ?

Vous vous reconnaissez ? Alors, découvrez notre offre :

CE QUE NOUS POUVONS ACCOMPLIR ENSEMBLE :

L’activité Systèmes terrestres et aériens conçoit des systèmes, des équipements, des capteurs et des services pour le contrôle du trafic aérien civil et militaire, et la défense aérienne.

Le site de Massy est leader dans les systèmes de commandement et de contrôle des opérations aériennes et les systèmes radars de défense aérienne.

Au sein d'un projet de dimension internationale, et d'une équipe de trois personnes réalisant l'automatisation des tests des interfaces utilisateurs de ce système, vous intervenez sur l'évaluation de méthodes pour la mise en œuvre d'assistant de preuves dans le cadre de cette automatisation.

À partir d'étapes de tests qui ont été automatisées à l'aide d'un langage impératif, il s'agit d'évaluer des méthodes basées sur des assistants de preuves pour prouver/évaluer la complétude de l'implémentation de tests automatisés.

En nous rejoignant, vos missions comporteront :

• L’analyse de tests et de la complétude des éléments d’information systèmes disponibles pour la mise en œuvre des méthodes de preuves de programme
• -L’analyse de l'adéquation des méthodes de preuves (why/logique de Hoare/Extraction de programmes) de programmes liés à l’automatisation de tests
• Un Choix/ une justification d'un exemple de test automatisé pour la mise en œuvre de la méthode why
• La mise en œuvre de la méthode why
• La rédaction d’un rapport d'évaluation

En fonction des résultats de l'évaluation, le déploiement de la méthode pourrait être appliqué à plus grande échelle, sur l'ensemble des tests automatisés, voire sur d'autres systèmes.

Innovation, passion, ambition : rejoignez Thales et créez le monde de demain, dès aujourd’hui.