Méthodologie formelle pour l'exploration et l'évaluation des architectures logicielles critiques complexes H/F

Description de l'offre : Le stage vise à améliorer la méthodologie outillée existante appelée QuaRTOS-DSE en renforçant la formalisation et la mise en œuvre de cette méthodologie. Il portera sur l'exploration et l'évaluation des architectures logicielles critiques complexes. Les architectures logicielles obtenues seront évaluées par une vérification formelle des propriétés extra-fonctionnelles du système à l'aide d'outils existants. L'exploration et l'évaluation des architectures logicielles critiques complexes se feront à l'aide d'un outil itératif (une première version avec une formalisation initiale de l'approche existe déjà), au niveau des fonctions, des tâches, des agents et des acteurs. Cette exploration intégrera des stratégies d'architecture à la pointe de l'état de l'art ainsi que les meilleures pratiques pour les logiciels critiques. L'approche devra inclure une évaluation de certaines métriques et un lien avec les outils d'évaluation. Le cadre existant présente des limitations, notamment une faible intégration du modèle matériel (HW), des restrictions sur la construction du modèle d'entrée (niveau d'abstraction), et des limites concernant la transformation/génération de modèles pour les outils d'évaluation et de vérification. Les principales activités du stage seront : Étudier/explorer l'existant (formalisation de la méthodologie et cadre existant) ; Identifier les limitations ; Identifier/trouver des APIs, des langages et des outils permettant d'améliorer l'interopérabilité du cadre existant afin de gérer davantage de modèles d'entrée, de niveaux d'abstraction, et d'outils d'évaluation et de vérification ; Développer une nouvelle version/mise en œuvre du cadre amélioré sur la base des cas d'utilisation existants. Durant ce stage, l'étudiant acquerra une expérience pratique avec les systèmes critiques de sécurité et les techniques de vérification formelle. Ce projet représente une opportunité précieuse pour développer des compétences clés dans la conception de systèmes critiques. L'utilisation d'outils d'IA générative pour la génération de code source sera également explorée au cours de ce stage.

Profil du candidat : Diplôme requis : Master (Bac+5) - Master of Science. Compétences : Compréhension des logiciels embarqués critiques. Connaissance des méthodes formelles (un plus). Maîtrise de l'anglais courant. Capacité à travailler en équipe, curiosité et esprit d'initiative. En accord avec l'engagement du CEA en faveur de l'intégration des personnes en situation de handicap, ce poste est ouvert à tous.

Diplome préparé : Bac+5 - Diplôme d'études approfondies (DEA)

Langues : Anglais Courant