Réalisation une interface graphique de preuve pro-active

Le but de ce stage est de concevoir et de réaliser une interface graphique permettant de manipuler des démonstrations sur des obligations de preuves de l’AtelierB.

L’AtelierB (voir https://www.atelierb.eu/) est un outil industriel permettant de développer des logiciels garantis sans défauts. Il est, par exemple, utilisé pour produire les systèmes de contrôle des métros automatiques de la ligne 1 et 14 de Paris. L’idée est de produire des critères de vérification du logiciel qui sont appelées « obligation de preuves » (OP). Ces OP sont ensuite analysées par un logiciel qui va démontrer qu’elles sont correctes de la même manière qu’on démontre un théorème mathématique mais de façon mécanisée « formelle ».

Lorsqu’une OP est trop complexe pour être comprise par l’outil, on rentre dans un mode interactif ou l’on va décomposer le problème en sous-problèmes plus simple jusqu’à ce que tout soit validé (ou que l’on ait identifié un bug). C’est le programme qui permet cette manipulation interactive qui fait l’objet du stage.

Actuellement, nous disposons d’un outil qui est globalement un terminal textuel agrémenté de panneau d’information, de boutons et de menus d’actions non contextuel (ou peu). L’utilisateur tape des commandes ou utilise des boutons et observe l’état de la preuve en lisant la conclusion et les hypothèses textuels formelles (comme un code source).

Points clés du stage :

  • cycle complet de développement à faire sur un nouvel outil
  • intégration de cet outil dans un atelier logiciel industriel
  • développement en C++ avec Qt
  • travail important sur la programmation de GUI (création de widget)
  • travail sur la manipulation d’un langage formel
Location
  • Paris
Duration 4 à 6
Level 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