Atelier B : utilisation de ProB pour la preuve de bonne définition

CLEARSY est une PME Française fondée en 2001 par les ingénieurs auteurs de l’industrialisation de l’outil de modélisation formelle appelé Atelier B, utilisé pour spécifier, concevoir, valider les systèmes et réaliser les logiciels critiques (comme le pilote automatique du métro de la ligne 14 à Paris).

Rassemblant 150 ingénieurs répartis sur 4 pôles (Aix – Paris – Lyon – Strasbourg) CLEARSY participe aux projets stratégiques des grands industriels et donneurs d’ordres nationaux et internationaux.
L’activité est majoritairement orientée vers les secteurs ferroviaire, énergie (nucléaire) et défense. CLEARSY exporte aujourd’hui son expertise et ses systèmes à l’étranger (Sao Paolo / Stockholm / Caracas / New York / Hiroshima / Honolulu…)

Dans le cadre d’utilisation de l’Atelier B les ingénieurs doivent garantir certaines contraintes sur la modélisation notamment sur la bonne définition mathématique des termes employés.

L’outil ProB a récemment fait des travaux sur des procédures spécialisées pour la preuve de bonne définition qui lui permettent d’avoir d’excellents résultats (réponses rapides).

Objectif :

Le stage aura comme objectif d’utiliser cette fonctionnalité pour améliorer l’utilisation d’Atelier B à plusieurs niveaux :

  1. Informations d’erreur de bonne définition visible dans l’éditeur de composants à chaque sauvegarde.
  2. Vérification de bonne définition au niveau des modèles (en complément des outils actuels).
  3. Vérification de bonne définition au niveau des commandes du prouveur interactif.

Livrables attendus :

  • Documentation mise à jour
  • Logiciels
  • Banc de test
  • Evaluation des différentes solutions

Profil:

  • C++
  • Rigueur, autonomie, force de propositions
  • Une première expérience des méthodes formelles et les solveurs serait un plus.
Location
  • Aix-en-Provence
Duration 6 mois
Level Bac +5

Postuler à cette offre de stage d'ingénieur

Pour postuler merci d’envoyer
un CV et une lettre de motivation
à l’adresse :

stages-ingenieurs@clearsy.com