Stages en informatique sécuritaire pour l’année 2014

Toutes les offres de stage pour 2014 sont pourvues,

nous vous proposons de nous retrouver dès l’an prochain !

Affichage de plan de voies signalisé par Compteurs D’essieux (POURVU)

Nous recrutons un(e) stagiaire pour le développement d’un affichage de Plan de Voies signalisé par Compteurs d’Essieux.

ClearSy développe des systèmes de comptage d’essieux sécuritaire SIL4 suivant la norme ferroviaire EN50129.Postuler Le compteur d’essieux est un dispositif assurant la même fonction qu’un circuit de voie, détecter la présence d’un train dans une zone. Cette information est fournis au système de signalisation dont la fonction est de protéger les trains, éviter tous risques de collisions entre les trains et tous risques de déraillement dans les aiguillages.

Le stage consiste à développer un prototype qui permettra l’affichage de l’état d’une ligne ferroviaire équipée de ces compteurs d’essieux en temps réel.
Le stagiaire devra développer une carte standard sur microcontrôleur (PIC) pour récupérer l’état de chaque zone a partir des informations du compteurs d’essieux et les afficher via un serveur web (Ajax) du microcontrôleur, ainsi que sur une application client sur PC.
La communication entre toutes les cartes PIC se fera en IP (couche basse IP déjà réalisée) et/ou en RS485 et chaque carte communiquera l’état de son rack compteur d’essieu à toutes les autres cartes du réseau.

Chaque carte recevra les informations de toutes les autres cartes afin de les afficher sur un écran programmable embarquée.

Le stage sera structuré comme un projet : spécification, développement, tests et documentation.

Environnement technique :  C++, Qt, Phyton. Les notions de ferroviaire seront dispensées lors du stage.

  • Localisation : Aix en Provence.
  • Niveau : Bac +4 / Bac +5
  • Durée : 5 à 6 mois

Création d’un enregistreur standard (POURVU)

Nous recrutons un(e) stagiaire pour le création d’un enregistreur standard.

Postuler

Clearsy développe des systèmes sécuritaires suivant la norme ferroviaire EN50129.
Dans le cadre de la mise en place de démonstrateur de produit dans le monde entier, Clearsy a besoin d’équipement permettant la traçabilité des évènements sur les produits déployés afin de pouvoir avoir des statistiques de fonctionnement et prouver sa fiabilité.

Le stage consiste à développer un enregistreur réutilisable sur de multiples projets. Le stagiaire devra développer une carte standard sur microcontrôleur (PIC) pour récupérer l’état de données d’entrées (analogique ou numérique). Cette carte stockera en interne les informations puis les téléchargera via IP sur un serveur de base de données. La mise en place du serveur et la création de la base de données fait partie du stage. La mise en place d’une interface DATA type 3G est à prévoir si le lieu d’installation des cartes PIC ne permettent pas un accès internet.

Environnement technique : Electronique, C, C++, Langage WEB (Javascript, Ajax, HTML), Base de données (SQL).

  • Localisation : Aix en Provence.
  • Niveau : Bac +4 / Bac +5
  • Durée : 5 à 6 mois

Développement d’un logiciel de génération graphique de Plans de Voies et d’objets ferroviaires (POURVU)

PostulerNous recrutons un(e) stagiaire pour le développement d’un logiciel de génération graphique de Plan de Voies et d’objets ferroviaires.

Pour de nombreux projets ferroviaires, nous vérifions les données liées aux caractéristiques des voies de lignes de métro. En 2013, nous avons conçu un outil de génération graphique de plans de voies à partir d’une base de données ainsi que la propriété inverse.
Le stage consiste à rajouter des fonctionnalités, à être capable de calculer et d’afficher des objets ferroviaires complexes, et de s’interfacer avec un second outil afin de mettre en évidence les données qui ne respectent pas les règles de sécurité des projets.

Plan du Stage :
Phase d’analyse : Le candidat devra intégrer les notions de ferroviaire dispensées et comprendre les capacités de l’outil existant. Il devra ensuite assimiler les besoins, et rédiger la spécification des nouvelles fonctionnalités à coder.
Phase de développement : Le candidat devra implémenter les nouvelles fonctionnalités et s’interfacer avec un autre outil pour pouvoir afficher les informations ainsi récoltées.
Phase de test : Toutes les fonctionnalités devront être testées afin de vérifier qu’elles correspondent à leur spécification.
Phase de documentation : Tout au long du stage, le candidat devra être en mesure de produire la documentation associée à la spécification, aux tests et à l’utilisation des nouvelles fonctionnalités de l’outil.

Environnement technique :  C++, Qt, Phyton. Les notions de ferroviaire et de méthode B seront dispensées lors du stage.

  • Localisation : Aix en Provence.
  • Niveau :  Bac +5
  • Durée : 5 à 6 mois

Stage M2 R&D : Résolution de conflits dans le cadre du raffinement Automatique pour la méthode B (POURVU)

Domaine: Mathématiques/ Informatique

Nous recrutons un(e) stagiaire pour la résolution de conflits dans le cadre du raffinement Automatique pour la méthode B.

Les méthodes formelles sont fondamentales pour s’assurer de la sûreté de fonctionnement de systèmes critiques. La méthode B est une des méthodes formelles appliquées  dans l’industrie (Ferroviaire, nucléaire, armée, automobile …). Elle est aussi reconnue académiquement (conférence ABZ…).

La méthode B consiste à simuler des systèmes puis à développer de manière consistante les logiciels supportant ce système. Un logiciel développé en B est prouvé correct par construction à l’aide d’outils de preuve semi automatisés traitant de la logique du premier ordre augmentée d’opérateurs ensemblistes (en d’autres termes, il s’agit de prouver des expressions mathématiques). Le principe de la construction est de partir d’une spécification formelle la plus abstraite possible collant aux spécifications papier/métier, puis de raffiner/préciser par étapes la manière d’implémenter. Ces différentes phases de raffinement sont prouvées correctes à l ‘aide des outils B. Enfin lorsque le logiciel (en langage B) est décrit suffisamment précisément, on peut générer du code C ou ADA qui est correct par construction vis à vis de la spécification formelle  abstraite de départ.

Un des problèmes de la méthode B est le temps (et donc le coût) de développement tant lors des  phases de raffinement que lors des preuves. Aussi la maintenance et l’évolution de logiciel ont montré une certaine lourdeur/inertie de la méthode.

Ainsi l’entreprise Clearsy qui maintient l’outil de développement AtelierB a récemment utilisé une méthode de raffinement automatique. Celle-ci évite certaines lourdeurs de la méthode B classique, mais introduit de nouveaux problèmes et challenges. Ce raffinement automatique utilise en quelque sorte des règles de raffinement/réécriture. Dans ce stage nous nous intéresserons à la la résolution de conflits lors du raffinement automatique en méthode B.

Alors que, dans la méthode classique, une variable abstraite se raffine d’un niveau à l’autre de raffinement car on travaille à un niveau d’abstraction donnée, le raffinement automatique focalise localement sur les opérations. Ainsi le raffinement de variable se fait à opération donnée. Ceci peut  entraîner des incohérences d’abstraction entre différentes variables et entre opérations (ex : si une opération op1 impose : «  la variable v1 doit rester abstraite et une autre variable v2 doit être raffinée » et inversement si l’opération op2 impose : « v2 doit rester abstraite et v1 dont être raffinée », alors un conflit ou une incohérence apparaît).    Actuellement ces conflits sont résolus par des règles ad-hoc qui peuvent potentiellement court-circuiter d’autre raffinements, et plus largement une réutilisation de l’outil de raffinement automatique. De plus le coût de résolution de ces conflits est non négligeable pour un utilisateur non averti. Alors que le raffinement automatique est censé simplifier le travail, d’autres problèmes réapparaissent et nécessite déjà une bonne pratique !  Il est donc nécessaire d’automatiser cette résolution de conflit.

Domaine : Mathématiques / Informatique

Intérêt pour  : Méthodes formelles, Logique,  Preuve, Algèbre, Sémantique, Algorithmie

Compétences nécessaires : Forte aisance intellectuelle dans l’abstraction mais aussi en codage C/C++, connaissance appréciée en B ou Coq , autonomie, efficacité.

Plan du stage :

 1°) Phase d’analyse (1,5 mois)

Le candidat devra s’approprier les principes généraux de la méthode B puis comprendre en détail par la théorie et la pratique l’actuel principe de raffinement automatique. Il devra ensuite lister les causes de conflits, lister l’intérêt et les inconvénients de ces causes de conflits vis à vis de l’effort de preuve/ de l’effort de typeCheck : en taille de code généré.

2°) Proposition d’algorithme (1 mois)

Le candidat devra proposer un algorithme permettant d’éviter les conflits en jouant sur différents paramètres tels que l’importation d’opération ou le relâchement temporaire de certaines règle de type check. L’algorithme doit être proche de l’optimal vis à vis des contraintes en effort de preuve et en typecheck et doit permettre d’être efficace dans un projet industriel et d’améliorer les performances de développement actuel.

 3°) Implémentation de l’algorithme (2 mois)

Le candidat devra adapter entièrement son algorithme au logiciel de raffinement automatique en le codant en C/C++/Qt.

 4°) Extension possible /Rédaction (1,5 mois)

Le candidat devra rédiger l’ensemble de sa démarche et pourra si le temps le permet attaquer/proposer des extensions possibles autres au logiciel de raffinement.

 

Nota Bene : L’encadrement sera effectué par des personnes expertes ou expérimentées, et principalement par des docteurs es sciences en informatique spécialité : logiques appliquées/ techniques de réécriture.

  • Localisation : Aix en Provence ou Paris
  • Niveau : Bac +5
  • Durée : 6 mois

Portage d’une application sécuritaire sous SCADE (POURVU)

Nous recrutons un(e) stagiaire pour le portage d’une application sécuritaire sous SCADE.

Clearsy développe des systèmes sécuritaires reposant sur des architectures à base de microprocesseurs et d’électronique de sécurité intrinsèque. Le stage consiste à porter une application existante (contrôle commande de porte palière de métro) en environnement SCADE.
Le stage sera encadré par un responsable expérimenté et est structuré comme un projet (revues, documents, développement, tests).

Environnement technique :  SCADE. Les notions de ferroviaire nécessaires seront dispensées lors du stage.

  • Localisation : Aix en Provence.
  • Niveau : Bac +4 / Bac +5
  • Durée : 5 à 6 mois

Les commentaires sont fermés.