Visualisation de contre-exemples dans l’éditeur 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é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 prouver un certain nombre d’obligations de preuves (théorèmes) de leur modèle. Des travaux récents dans le cadre d’un projet de recherche ont permis de connecter des nouveaux prouveurs afin de valider ces obligations de preuve.

Cette intégration permet notamment de lancer des prouveurs externes « SMT » sur une obligation de preuve donnée, et d’en visualiser la sortie lorsqu’un contre-exemple est trouvé.

Objectif

Le but du stage serait de faire en sorte que la visualisation du contre-exemple soit réalisée sur les objets du modèle plutôt que sur les objets du prouveur.

Cela passe par une instrumentation des outils de génération d’obligation de preuve avec des informations de traçabilité, par une éventuelle adaptation des requêtes envoyées aux prouveurs externes pour que ceux-ci fournissent une information mieux ciblée, et par un travail d’amélioration de l’interface graphique pour ce qui est de la présentation des résultats.

Dans un deuxième temps, il serait également possible de prototyper de nouveaux schémas d’encodage vers les prouveurs externes, ou cibler d’autres prouveurs externes (ProB, par exemple).

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