Outillage pour la validation de règles de preuve de l’Atelier B

Description

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é 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 de développement logiciel avec la méthode B les ingénieurs sont parfois amenés à ajouter des règles manuelles (mathématique) de preuve.

Ces règles font l’objet d’une validation qui peut être :

  • Automatique : avec l’outils Prouveur de Prédicat (PP)
  • Manuelle : par une preuve et sa vérification Dans l’Atelier B l’outil OPR et son interface graphique OPRGUI permettent la gestion projet de ces règles.

Objectif

Ce stage a pour objectif d’étendre l’outil OPR et son interface pour permettre d’utiliser d’autres prouveurs mathématiques que le prouveur de prédicat pour vérifier des règles de preuve, afin de réduire les règles à valider manuellement.

Ces prouveurs mathématique sont en partie ceux inclue dans l’AtelierB (y compris, donc, le prouveur interactif), et des prouveurs automatiques tiers (solveurs SMT, ProB). On est aussi bien intéressé par des résultats positifs (la règle est prouvée valide), que par des résultats négatifs (la règle est prouvée fausse et un contre-exemple est exhibé).

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