OUTIL DE VALIDATION FORMELLE

Objectif du stage : Utilisation d’un model-checker pour de 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).
L’activité est majoritairement orientée vers le secteur ferroviaire, énergie (nucléaire) et défense.

Société à taille humaine sur 4 sites en France, en pleine croissance (150 personnes), nous développons et déployons nos systèmes dans le monde entier depuis plus de 10 ans, nous avons notamment pu travailler à Sao Paolo / Stockholm / Caracas / New York / Hiroshima / Honolulu…)

Les équipes CLEARSY interviennent dans toutes les phases d’un projet, de la spécification à la réalisation de systèmes « clé en main » tout en garantissant un respect le plus strict des exigences de sûreté.
Clearsy recherche aujourd’hui des ingénieurs passionnés par le challenge technique et qui ont appris à apprendre pour venir renforcer ces équipes techniques.

Cette citation reflète bien nos valeurs : Steve Jobs – Cela n’a pas de sens d’embaucher des gens intelligents et de leur dire quoi faire ; nous embauchons des gens intelligents pour qu’ils nous disent ce qu’il faut faire

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 :

Informations d’erreur de bonne définition visible dans l’éditeur de composants à chaque sauvegarde.
Vérification de bonne définition au niveau des modèles (en complément des outils actuels).
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.

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

Pour postuler merci d’envoyer un Cv et une Lettre de motivation à l’adresse : stages-ingenieurs@clearsy.com