Concepteur d'architectures de supervision dédiées aux systèmes distribués - CDD - Paris-Saclay W/M

Description de l'offre : Rejoignez le CEA pour donner du sens à vos travaux, diriger et soutenir des projets de R&D nationaux et internationaux, nourrir et attiser votre curiosité. EN RÉSUMÉ, QUE VOUS PROPOSONS-NOUS ? La vérification d'exécution (RV) est à la croisée de la vérification formelle et de la surveillance. Elle consiste à analyser les exécutions du système, telles qu'observées au moyen d'un monitoring architecture, afin de vérifier leur conformité à un modèle de référence formel, caractérisant l'ensemble des comportements acceptables du système. Lorsqu'il s'agit de systèmes distribués, la capacité d'une technique RV à analyser les flux de communication entre les sous-systèmes est un élément central, puisque les systèmes distribués sont composés de sous-systèmes déployés sur différentes machines et interagissant par transmission de messages pour exécuter des services. Cette capacité repose d'abord sur l'expressivité du langage utilisé pour spécifier les modèles de référence formels. Il s'agit essentiellement de pouvoir modéliser des communications asynchrones entre processus concurrents. Cela est possible dans une grande variété de formalismes, y compris les formalismes dérivés des diagrammes de séquence de messages (MSC) et des diagrammes de séquence UML (UML-SD). Nous appelons ces modèles "interactions". Le CEA LIST développe le MAAT IAT (Interaction Analysis Tool) pour analyser les exécutions de systèmes distribués et les confronter aux interactions. Lorsque le système est en cours d'exécution, les traces d'exécution sont enregistrées sur chacun des sous-systèmes. Les traces de tous les sous-systèmes sont rassemblées dans un tuple de traces, qui est ensuite analysé par un algorithme RV. Les principes de cette approche sont détaillés dans plusieurs publications [1,2]. Il existe deux types d’approches RV : les approches hors ligne et en ligne. Dans les approches hors ligne, les exécutions observées sont collectées a priori lors d'une phase de journalisation, tandis que dans les approches en ligne, le processus de vérification interagit en permanence avec l'architecture de surveillance. VOTRE MISSION : La précision des informations calculées par un algorithme RV dépend de la précision des observations des exécutions du système. Lorsqu'il s'agit de vérification d'exécution en ligne, ces observations sont réalisées via ce que l'on appelle une architecture de surveillance. L'architecture de surveillance doit être fiable, c'est-à-dire éviter la perte d'informations, et suffisamment rapide pour permettre à l'algorithme RV d'effectuer son analyse le plus rapidement possible, en essayant de faire face à la fréquence des observations imposée par l'exécution du système. L'une des limites pratiques du RV en ligne est que, pour des raisons économiques, il n'est souvent pas possible de concevoir et de mettre en œuvre une architecture de surveillance complète à partir de zéro, pour chaque nouveau système à vérifier. Il est donc souhaitable de concevoir une bibliothèque générique de fonctionnalités de surveillance pouvant être utilisée à cette fin. Vous contribuerez à la conception et à la mise en œuvre d'une telle bibliothèque pour l'outil MAAT IAT.

Langues : Anglais Courant