L’Atelier B est formé d’un cœur, ensemble d’outils assurant les activités liées à la preuve logicielle, et d’interfaces humain-machine (IHM), permettant d’orchestrer les outils du cœur. Dans le cadre de sa démarche qualité logicielle, CLEARSY cherche à mettre en place un banc de tests automatisé des IHM de l’Atelier B.
Le but principal de ce stage est de réaliser la nouvelle IHM de cet outil. Cette nouvelle IHM devra améliorer l’expérience utilisateur du démonstrateur tout en adhérant à la nouvelle identité visuelle de CLEARSY.
L’objectif du stage est de réaliser un audit de nos systèmes et de voir comment ces normes s’imposent à ceux-ci. Il faudra déterminer quelle est leur conformité actuelle et quelles seraient les modifications techniques / organisationnelles à apporter. Les concepts qui s’appliquent à ce sujet, les exigences requises et un plan d’amélioration préliminaire et résultats seront compilés dans un rapport.
L’objectif du stage est de développer un démonstrateur de la fonctionnalité Secure Boot, sur une architecture à déterminer (faisabilité parmi une architecture à base de microcontrôleur ou de processeur) et à justifier.
Il s'agit de concevoir des modules d'entrées sécuritaires à bas coût. Le stage se décompose comme un projet que le stagiaire devra prendre en charge en toute autonomie (accompagné de son tuteur et de l’équipe CLEARSY).
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). Le stage a comme objectif d’utiliser cette fonctionnalité pour améliorer l’utilisation d’Atelier B.
Nos ingénieurs doivent prouver un certain nombre d’obligations de preuves de leur modèle. Des travaux récents ont permis de connecter des nouveaux prouveurs afin de valider ces obligations de preuve et d’en visualiser la sortie lorsqu’un contre-exemple est trouvé. 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.
Ce stage a pour objectif d’étendre l’outil Outil Preuve de Règles 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.