Cet apprentissage s’inscrit dans le domaine de l’ingénierie des langages logiciels et des outils de développement de langages dédiés (DSLs). Il vise à automatiser, à partir d’une représentation graphique (e.g., via PlantUML), la création d’artefacts permettant de générer un langage textuel (via Langium) et aussi de permettre de donner des représentations visuelles ou conceptuelles des programmes définis dans ce langage (e.g., via Sprotty ou KlighD).
L’apprentissage se déroulera dans un cadre académique, sur une durée de 1 à 2 ans (M1 + M2 ou M2 seul), avec des perspectives de recherche appliquée, publication scientifique et/ou valorisation open source.
💬 Remarque importante pour les candidats
Ce sujet couvre un large spectre de recherche, mais ne vous inquiétez pas : vous ne serez jamais seul. Le travail commencera par des objectifs clairs, progressifs et atteignables, adaptés à votre niveau (M1 ou M2), avec un encadrement régulier pour vous guider à chaque étape.
L’apprentissage comporte deux axes complémentaires à explorer :
Il existe un lien clair entre une grammaire et une représentation object, popularisé au travers de Xtext. On veut dans un premier temps porter ce savoir dans le monde de l’ingénérie des langages avec VSCode.
Pour cela on propose d’utiliser Langium et PlantUML de deux manières complémentaires.
Langium est un outil permettant la création d’un IDE (extension VSCode) à partir de la description d’un grammaire. Cette grammaire est actuellement définie sous une forme nommée BNF. À parti de cette BNF, Lagium génère du code TypeScript qui suit une structure orientée objet (interfaces, types, héritages).
Le premier objectif consiste à générer automatique une grammaire Langium à partir d’un diagramme de classe.
Le second objectif consiste à produire automatiquement un diagramme de classes UML à partir d’une grammaire BNF (ou du code TypeScript).
Cela permet de mettre en avant le modèle du domaine visé par le langage, c’est à dire ses concepts et leurs relations, plutot que de mettre en avant la manière textuelle permettant d’écrire des programmes pour ce domaine.
Résultats attendus :
Langium permet de rapidement définir des environnement de développement textuels à partir de la grammaire d’un langage. KlighD et Sprotty permettent de définir facilement des diagrammes représentatifs d’une application. On aimerait pouvoir facilement lier KlighD ou Sprotty et Langium afin d’obtenir un environnement de développement qui permette de définir des programmes textuellement mais aussi d’obtenir une (ou plusieurs) représentations graphiques de ces programmes. Cette objectif est dans une certaine mesure addressé par Sirius mais l’équivalent n’existe pas dans la galaxie VSCode.
L’objectif premier est de fournir une représentation graphique basique, automatiquement générée à partir de la grammaire. Ensuite l’objectif est de fournir un meta langage (ou un système d’annotations) qui enrichit une grammaire Langium afin de définir comment ses éléments doivent être visualisés graphiquement (noeuds, liens, dispositions). La représentation visuelle pourra par exemple être générée avec le framework Sprotty.
Résultats attendus :
Envoyer CV, lettre de motivation et relevés de notes (si disponibles) à l’adresse ci-dessus.
.
.
.
.
.
.
.
.
.
Les débogueurs omniscients permettent de naviguer dans le passé d’un programme en conservant une trace de toutes les valeurs manipulées. Cette approche a montré son utilité dans de nombreux cas, mais elle repose souvent sur des exécutions déterministes et des valeurs exactes.
Or, dans de nombreux systèmes modernes (systèmes embarqués, systèmes distribués, applications temps réel ou IA), les données manipulées sont incertaines : elles sont issues de capteurs bruités, de temporalités non parfaites ou encore de modèles approximatifs. L’exécution du programme dépend donc non seulement du code, mais aussi de valeurs observées sujettes à interprétation, ainsi que de temporalités floues ou concurrentes.
Cet apprentissage propose de repenser l’expérience du débogage à travers le prisme de l’incertitude, dans une optique à la fois scientifique, pratique… et un peu (plus) ludique :).
💬 Remarque importante pour les candidats
Ce sujet couvre un large spectre de recherche, mais ne vous inquiétez pas : vous ne serez jamais seul. Le travail commencera par des objectifs clairs, progressifs et atteignables, adaptés à votre niveau (M1 ou M2), avec un encadrement régulier pour vous guider à chaque étape.
L’objectif principal est de concevoir une nouvelle génération de débogueur qui intègre des incertitudes temporelles (délai, latence, timestamps flous) et les exposes au développeur pour lui permettre de mieux comprendre son programme. Le débogueur doit aussi intègrer des incertitudes de valeur (valeurs bruitées, intervalles, distributions) et permette une visualisation et interaction intuitive, exploratoire et narrative (e.g., navigation dans des “chemins plausibles”, infobulles de confiance, arbres alternatifs).
Plus concrètement, l’apprentissage se structurera autour de deux axes :
Il s’agira d’analyser et représenter des exécutions avec incertitude, cela signifie fournir une modélisation de traces enrichies avec des intervalles d’incertitudes, des temporalités movantes, des événements alternatifs, etc permettant une meilleure compréhension des phénomènes sous jacents. Il s’agit aussi de fournir une visualisation graphique et narrative d’exécutions multiples ou floues et d’y attacher des interaction pour explorer les causes possibles d’un comportement.
Sur la base d’un moteur existant (e.g., moteur de trace de studio GEMOC, d’un langage existant ou d’un mini DSL utilisant le Debug Adapter Protocol (DAP)), il sera nécessaire de construire un prototype de débogueur interactif intégrant un système de navigation dans des timelines floues, la possibilité de comparer deux exécutions (ou deux chemin d’exécution) et une intégration avec les protocoles classiques de type Debug Adapter Protocol intégré dans VScode.
Envoyer CV, lettre de motivation et relevés de notes (si disponibles) à l’adresse ci-dessus.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
Dans de nombreux systèmes logiciels modernes, on combine différents types de modèles pour raisonner, simuler, diagnostiquer ou prédire. Ces modèles peuvent être déductifs, i.e., basés sur des règles, équations ou abstractions formelles ou bien inductifs, issus de données, via apprentissage statistique ou machine learning.
L’hybridation de modèles est au coeur de nombreux travaux actuels (jumeaux numériques, systèmes cyber-physiques, IA explicable, etc.). Il est aujourd’hui important de refléchir à comment définir de manière correcte ces hybridations. Pour ce faire, il semble nécessaire de fournir une manipulation unifiée des modèles permettant ainsi de manipuler génériquement les modèles déductifs et inductifs lors du processus d’hybridation. C’est une challenge qui reste difficile, car :
Chaque modèle repose sur un formalisme ou une structure propre. Pour les modèles déductifs, il s’agit typiquement de sa grammaire (BNF), d’arbres syntaxiques, ou de méta-modèles explicites. Pour les modèles inductifs, cette structure est souvent implicite (e.g., architecture du réseau neuronal, structure d’arbre, pipeline de traitement), voire non formalisée, bien qu’elle existe (ONNX, PMML tentent de la capturer).
Chaque modèle possède des paramètres de nature différente. Habituellement symboliques ou typés dans les modèles déductifs (types, contraintes, opérateurs…). Plutôt numériques ou statistiques dans les modèles inductifs (poids appris, biais, hyperparamètres…).
Enfin, chaque modèle est manipulé avec des outils ou formats spécifiques. On parle ici des outils de transformation ou d’édition dans le cas de DSLs ou de systèmes à règles; et d’APIs de frameworks variés pour les modèles appris (scikit-learn, TensorFlow, PyTorch), sans standard de manipulation ou d’interrogation universel.
Il n’existe pas, à ce jour, d’interface commune permettant de créer, modifier, interroger, ou composer ces modèles quel que soit leur type, ce qui ne permet pas d’aller vers une systématisation du processus d’hybridation.
Cet apprentissage vise donc à explorer le concept de “Modelling Activity as a Service”; c’est à dire de considérer la création, manipulation, transformation ou exécution de modèles comme des services standardisés, orchestrables, et indépendants de la nature du modèle lui-même.
💬 Remarque importante pour les candidats
Ce sujet couvre un large spectre de recherche, mais ne vous inquiétez pas : vous ne serez jamais seul. Le travail commencera par des objectifs clairs, progressifs et atteignables, adaptés à votre niveau (M1 ou M2), avec un encadrement régulier pour vous guider à chaque étape.
L’objectif de cet apprentissage est d’explorer le concept de “Modelling Activity as a Service” (MAaaS), qui vise à offrir des services génériques de création, lecture, mise à jour, suppression, transformation ou exécution de modèles, quelle que soit leur nature (déductive ou inductive). Il sera également nécessaire de rendre ces services accessibles via des interfaces standardisées et qui pourrait être paramètrées la description du langage / de la structure.
Définir une vue abstraite et unifiée des modèles, i.e., d’une part étudier si une forme de méta-modèle générique ou de représentation intermédiaire (ex : graphe typé, structure hiérarchique, JSON enrichi…) peut servir de socle commun; et d’autre part intégrer des méta-informations comme le type (inductif vs déductif), les paramètres ou les contraintes.
Définir des services de manipulation afin de permettre différentes manipulations comme par exemple la création de nouveaux modèles (par langage ou type), l’interrogation et la modification de leurs propriétés,la transformation ou l’évaluation des modèles (ex. exécution, entraînement, simulation),la composition ou hybridation (fusion de modèles hétérogènes), ou encore l’introspection de ces modèles. Ces services pourrait être fournis comme une APIs REST/GraphQL ou via un moteur de requêtes modèle.
Envoyer CV, lettre de motivation et relevés de notes (si disponibles) à l’adresse ci-dessus.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
Les jumeaux numériques (Digital Twins - DT) sont aujourd’hui au coeur des stratégies de simulation, de supervision et d’optimisation de systèmes physiques complexes. Ils permettent de créer une réplique numérique d’un système réel, connectée aux capteurs et fournissant plus ou moins de service. Par exemple un DT simple (souvent nommée Digital Shadow) fournit un suivi de l’état du système physique dans une interface numérique. Cela permet de suivre l’évolution du système physique. On peut toutefois aller plus loin et des modèles déductifs (basés sur des règles ou des abstractions formelles) qui permette par exemple de contrôler tout ou partie du système physique, utilisant le système physique comme un service. Enfin, on peut encore compléter le DT en intégrant des modèles inductifs (appris à partir de données) qui permette de faire des opérations de prédiction ou de comparaison de comportement.
Cet apprentissage s’inscrit dans l’étude et l’expérimentation des DT à l’échelle d’un système pédagogique physique : une usine miniature Fischertechnik. Elle reproduit à petite échelle des éléments typiques d’une ligne de production automatisée (capteurs, actionneurs, convoyeurs, tris…).
Cette micro-usine fournit un terrain idéal pour expérimenter l’instrumentation et la récolte de données en temps réel, l’obtention de modèles statistiques (inductifs), le pilotage ou la simulation par un DT modulaire et la co-évolution entre le système réel et ses abstractions.
💬 Remarque importante pour les candidats
Ce sujet couvre un large spectre de recherche, mais ne vous inquiétez pas : vous ne serez jamais seul. Le travail commencera par des objectifs clairs, progressifs et atteignables, adaptés à votre niveau (M1 ou M2), avec un encadrement régulier pour vous guider à chaque étape.
L’objectif de l’apprentissage est d’explorer la conception et l’implémentation d’un jumeau numérique modulaire et extensible pour cette usine miniature. L’apprenti sera amené à concevoir l’architecture du jumeau numérique et à développer les différents modèles et services de ce jumeau.:
La conception de l’architecture du jumeau numérique implique en premier lieu d’identifier et de caractériser les composants physiques et logiques du système réel; et de communiquer avec ceux-ci. Ensuite, il s’agira de proposer une architecture de DT qui puisse évoluer, commençant par un Digital Shadow et en allant potentiellement jusqu’à articuler des modèles déductifs (e.g., logique de contrôle, règles d’ordonnancement, évaluation de l’énergie consommée) et des modèles inductifs (e.g., prédiction de performances, apprentissage de comportements, détection de dérive comportementale). Enfin, l’architecture devra être telle qu’elle permet de définir les protocoles de synchronisation entre l’état réel et l’état simulé.
Une fois l’architecture définie, il faudra : implémenter des modèles déductifs à l’aide de langages de modélisation ou de DSLs adaptés, collecter des données d’exécution de l’usine pour entraîner des modèles inductifs simples (e.g., classification, détection d’anomalies, estimation de durée). Ensuite les services du DT pourront être défini pour fournir des services telle que des prédiction ou autre. Enfin, il pourrait aussi être possible de fournir des modèles 2D/3D ou des dashboards qui permettent de visualiser l’évolution de l’usine en temps réel dans le monde virtuel.
Le but de ces travaux va au delà de l’obtention du jumeau numérique et il sera important de documenter les bonnes pratiques, les difficultés d’intégration rencontrées, et les limites actuelles des modèles et de l’architecture.
Enfin, on aimerait, in fine, produire un démonstrateur ou prototype interactif du jumeau numérique.
Envoyer CV, lettre de motivation et relevés de notes (si disponibles) à l’adresse ci-dessus.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
Dans les systèmes cyber-physiques, il est fréquent d’observer des divergences de comportement entre ce qui est attendu et ce qui est réellement produit. Ces divergences peuvent avoir de multiples causes : valeurs incertaines (capteurs bruités), exécutions non déterministes, effets de concurrence, ou erreurs de modélisation, variations comportementales dues à l’environnement (ex. obstacle inattendu, capteur dégradé),ou d’une incompréhension des exigences elles-mêmes.
Dans un tel contexte, l’enjeu n’est pas seulement de détecter qu’une divergence a lieu, mais de comprendre pourquoi – c’est-à-dire de formuler des hypothèses plausibles expliquant le comportement observé. Ce raisonnement relève de l’abduction, une forme de raisonnement inverse consistant à proposer les causes les plus probables d’un effet observé, potentiellement à partir de traces incertaines et de comportements flous.
Cet apprentissage propose d’explorer la construction d’un outil de diagnostic capable d’assister un développeur confronté à des divergences. L’idée est de générer des hypothèses explicatives et de les présenter sous une forme interactive, narrative et utile.
💬 Remarque importante pour les candidats
Ce sujet couvre un large spectre de recherche, mais ne vous inquiétez pas : vous ne serez jamais seul. Le travail commencera par des objectifs clairs, progressifs et atteignables, adaptés à votre niveau (M1 ou M2), avec un encadrement régulier pour vous guider à chaque étape.
L’objectif principal est de créer un système de diagnostic comportemental sous incertitude, fondé sur un moteur abductif capable de raisonner sur des exécutions floues ou alternatives, et de fournir au développeur des hypothèses classées, visualisables et explorables.
Le travail s’organisera autour de deux grands axes :
Il s’agira d’identifier et modéliser des écarts entre un comportement attendu issus des exigences (spécification, trace de référence) et un comportement observé (exécution réelle ou simulée).
Cette modélisation devra tenir compte de l’incertitude sur les valeurs (intervalles, distributions), la temporalité (timestamps flous, ordonnancement non-déterministe) et les effets de concurrence.
À partir de la divergence détectée, le système devra être capable de raisonner à rebours et de proposer des scénarios explicatifs (causes possibles, effets secondaires, hypothèses environnementales).
Cela nécessite de s’appuyer sur des modèles de raisonnement abductif (e.g., graphe causal, logique abductive probabiliste) et de construire une interface de présentation des hypothèses, avec visualisation narrative, évaluation de plausibilité, et interaction avec l’utilisateur (filtrage, classement, hypothèses alternatives).
TODO
Envoyer CV, lettre de motivation et relevés de notes (si disponibles) à l’adresse ci-dessus.
.
.
.
Ce sujet est en lien avec les travaux du projet ANR TAPAS (Time-Aware Proof ASsistants [1]). L’objectif général de TAPAS est de fournir un cadre open source de modélisation, de validation et de vérification, ainsi qu’une méthodologie pour la conception de systèmes cyber-physiques fiables, depuis les exigences jusqu’au déploiement du code, en intégrant à un langage formel générique des outils d’analyse performants. TAPAS fait le choix de la modélisation et les outils Event-B en proposant des extensions pour la prise en compte d’exigences temporelles multiformes.
Event-B[2] est une méthode formelle destinée à la modélisation et à la vérification de systèmes informatiques et embarqués. Fondée sur la logique du premier ordre et la théorie des ensembles, Event-B repose sur deux concepts clés : les machines, qui décrivent la dynamique du système via des événements, et les contextes, qui définissent les entités statiques telles que les constantes et les axiomes. Le raffinement permet de développer progressivement un système depuis un modèle abstrait jusqu’à une implémentation concrète, tout en assurant la cohérence grâce à la génération automatique d’obligations de preuve.
Toutefois, Event-B adopte une vision globale du temps, souvent implicite ou représentée de manière abstraite, ce qui limite son aptitude à modéliser des systèmes complexes où plusieurs composants évoluent selon des temporalités distinctes, comme c’est le cas des systèmes cyber-physiques.
L’objectif de l’apprentissage est d’identifier les exigences nécessaires à une extension du formalisme Event-B en vue de supporter des systèmes à horloges multiples. Pour cela, seront réalisés une étude comparative d’exemples représentatifs de systèmes embarqués à temporalités différenciées ainsi qu’une évaluation de la méthode Event-B au travers de la plateforme Rodin [3].
L’organisation du stage pourrait prendre la forme suivante :
L’idée est de vous familiariser avec le langage Event-B et la plateforme Rodin au travers d’exemples simples dans un premier temps, qui permettront de vous approprier la méthode Event-B, la notion de preuve d’obligation et leur simulation. Dans un deuxième temps vous irez explorer des fonctionnalités plus avancées telles que la gestion des théories, les notions de raffinement progressifs. Le but de cette phase est d’identifier les forces et limites d’Event-B et de Rodin (exemple : modularité, gestion du temps, ergonomie de l’outil) dans le but de la troisième phase du stage mais aussi dans un objectif de restitution à l’équipe. Une attention particulière sera portée à la manière dont Event-B et Rodin supportent la gestion des exigences non fonctionnelles, notamment temporelles.
Plusieurs cas d’études de systèmes embarqués temps réel ont été sélectionnés dans le projet TAPAS. Ces uses case sont extraits des challenges de modélisation proposés dans le cadre de la conférence ABZ [4]. Parmi ceux-là nous avons retenu trois d’entre eux de différents domaines :
Le travail consiste en une analyse de ces exemples dont certains ont déjà donné lieu à une modélisation en Event-B. Il faudra identifier les exigences temporelles spécifiques aux différents systèmes et la prise en compte de ces exigences dans Event-B. Le résultat de cette phase sera la formulation d’un ensemble structuré d’exigences fonctionnelles temporelles auxquelles une extension multi-horloges d’Event-B devrait répondre dans le cadre de la modélisation de ces cas d’études.
L’idée ici est d’utiliser la base d’exigences identifiées dans la phase 2 pour développer une série d’exemples illustrant (ou pas) la modélisation et la vérification de comportements temporels en explorant les capacités de Rodin en matière de modélisation et de preuves.
Ces expérimentations se feront soit au travers d’exemples ciblés extraits des cas d’études soit en en donnant une version simplifiée. Le résultat de cette dernière partie peut être vue comme une sorte de benchmark temporel de Rodin. Il s’agira de documenter en les catégorisants :