Modélisation formelle : un livrable clé pour des modèles plus fiables et innovants
Le projet Archi-CESAM, soutenu par le PEPR Cloud, vient de livrer un document intitulé : « Description of the Targeted Formal Modeling Languages and their Semantics ». Rédigé par Zachary Assoumani, doctorant dans l’équipe CONVECS, ce document présente un panorama des langages utilisés pour la description et la vérification des architectures matérielles.
Pourquoi c’est important ?
Les langages de modélisation servent à créer des représentations simplifiées de systèmes complexes (un réseau électrique, un trafic aérien, etc.). Mais pour que ces modèles soient utiles, il faut leur donner une « sémantique » claire : en gros, définir précisément ce qu’ils représentent et comment les interpréter.
Le livrable L4.1, préparé par Zachary Assoumani, présente un ensemble des méthodes rigoureuses pour y parvenir, en citant les travaux de recherche correspondants. L’objectif ? Faciliter aux ingénieurs et chercheurs d’adopter les bonnes pratiques dans la conception de circuits optimisés pour les applications cloud en faisant des choix éclairés.
Zachary Assoumani, auteur de ce livrable, a récemment passé avec succès son premier comité de suivi de thèse, en présence d’Alexandre Duret-Lutz, expert renommé en vérification formelle. Zachary a également présenté les résultats de son analyse formelle de la spécification d’un cache haute performance lors du RISC-V summit Europe à Paris.
Et si demain, grâce à ces avancées, nos systèmes devenaient plus sûrs et plus intelligents ?