Stage de recherche M2 / dernière année d’école d’ingénieurs - 6 mois

Validation de modèles de simulation grâce aux méthodes formelles
Application aux modèles DEVS décrits dans le langage FDEVSML

• Laboratoire : LAAS-CNRS, Toulouse.
• Équipe d’accueil : TRUST — Trustworthy systems: foundations and practices, avec co-encadrement par l’équipe ISGE.
• Encadrants : Dr Clément Foucher (TRUST), Dr Luiz Villa (ISGE), Dr Silvano Dal Zilio (TRUST).
• Période prévue : du 1er février au 31 juillet 2027.
• Profil : Master 2 ou dernière année d’école d’ingénieurs en informatique, génie mathématique ou formation équivalente.

Le stage en quelques mots

Un modèle de simulation décrit comment un système évolue au cours du temps. Une syntaxe formelle permet de décrire le modèle dans un langage mathématique. Couplée à des algorithmes d’exécution également formels, la simulation du modèle peut alors être entièrement exprimée sur des bases mathématiques.

Mais comment s’assurer que l’évolution subie par un modèle au cours de la simulation respectera les contraintes définies ? Par exemple, la description formelle du modèle déclare un espace d’états autorisés pour l’état interne d’un modèle sous la forme d’un ensemble. Comment s’assurer que l’état du modèle ne sortira jamais de cet ensemble quels que soient les changements d’état successifs au cours de la simulation ?

L’objectif du stage est de développer un prototype capable de vérifier certaines de ces contraintes à l’aide de méthodes formelles : des outils mathématiques et informatiques permettant de démontrer des propriétés ou de rechercher des contre-exemples.

Vous commencerez par des modèles simples. Avec les encadrants, vous choisirez ensuite une méthode adaptée et évaluerez ce qu’elle permet de garantir, ainsi que ses limites.

1. Un exemple pour comprendre le problème

Imaginons un modèle de compteur :

• son état est un entier compris entre 0 et 10 ;
• à chaque événement, une règle augmente sa valeur de 1.

Que se passe-t-il lorsque le compteur vaut déjà 10 ? Si aucune condition ne l’empêche, la règle produit 11 : le modèle ne respecte plus l’espace d’états qu’il a lui-même déclaré.

Cette erreur peut exister même si la description du modèle est conforme au formalisme et manipule bien des entiers. Vérifier la syntaxe et les types ne suffit donc pas nécessairement à vérifier toutes les contraintes du modèle.

Le stage vise à détecter ce type d’incohérence par un raisonnement sur les règles du modèle, sans se limiter à observer quelques simulations.

2. Le contexte scientifique et les outils existants

Le stage porte sur DEVS et Parallel-DEVS, des formalismes de modélisation permettant de décrire des systèmes selon un paradigme à événements discrets : un système possède un état, reçoit des événements, produit des sorties et évolue selon des règles de transition.

Le langage FDEVSML permet d’écrire ces modèles mathématiques sous forme informatique. On y précise notamment :

• les états possibles du système ;
• les entrées qu’il peut recevoir et les sorties qu’il peut produire ;
• les règles de changement d’état ;
• le délai avant le prochain événement interne.

Des modèles élémentaires, appelés modèles atomiques, peuvent être assemblés en modèles couplés.

La chaîne d’outils FT4DEVS dispose déjà d’un analyseur qui transforme le texte FDEVSML en une représentation structurée et typée : un arbre syntaxique abstrait, ou AST. Vous pourrez vous appuyer sur cette représentation ; il ne s’agit pas de développer un nouvel analyseur.

L’étape étudiée pendant le stage consiste à vérifier des propriétés du comportement décrit par ces modèles. Une spécification du langage et des modèles d’exemple sont disponibles.

Il n’est pas nécessaire de connaître DEVS ou FDEVSML avant de candidater. Leur prise en main fait partie du stage.

3. La question de recherche

Comment vérifier automatiquement qu’un modèle respecte les contraintes qu’il déclare ?

Le premier objectif sera la préservation des domaines :

• une transition produit-elle toujours un état appartenant au domaine déclaré ?
• une sortie appartient-elle toujours au domaine de sorties prévu ?

Les hypothèses seront rendues explicites : états initiaux, entrées admissibles et conditions d’application des transitions. Vous distinguerez notamment la vérification d’une règle pour tous les états autorisés de l’étude des seuls états effectivement accessibles depuis un état initial.

Selon l’avancement, le travail pourra ensuite porter sur des propriétés temporelles : délais non négatifs, conditions d’application d’un événement externe ou traitement d’événements simultanés. Ces propriétés seront définies précisément avec les encadrants avant leur mise en œuvre.

4. Ce que vous ferez concrètement

Votre travail combinera lecture scientifique, raisonnement mathématique, programmation et expérimentation.

Vous serez amené·e à :

1. Comprendre quelques modèles simples, puis identifier les erreurs que l’on souhaite détecter.
2. Formuler les propriétés à vérifier et les hypothèses nécessaires.
3. Choisir une méthode avec les encadrants, à partir de premiers essais.
4. Développer un prototype sur une partie clairement délimitée du langage.
5. L’évaluer sur des exemples, comprenant des modèles corrects et des modèles volontairement erronés.
6. Analyser les résultats : garanties obtenues, contre-exemples, cas non pris en charge et situations où l’outil ne permet pas de conclure.

Deux pistes principales sont envisagées :

Solveur logique, par exemple Z3 (SMT) : Traduire les règles et contraintes du modèle en formules logiques, puis demander au solveur de rechercher une violation. Exemple : Rechercher un état autorisé depuis lequel une transition peut produire une valeur hors du domaine.

Assistant de preuve, par exemple Rocq : Définir mathématiquement les constructions du langage et établir des preuves vérifiées par machine. Par exemple, démontrer que certaines conditions sur un modèle suffisent à garantir la préservation de son domaine d’états.

D’autres pistes pourront également être envisagées, telle que la traduction du modèle DEVS en réseaux de Petri temporisés pour mener une étude à l’aide de la boîte à outils TINA.

Il n’est pas attendu de développer plusieurs solutions complètes. Une approche principale sera retenue avec les encadrants. Une comparaison ou une combinaison pourra être étudiée si elle apporte un bénéfice dans le temps disponible.

L’efficacité et les limites de chaque méthode font partie des questions de recherche : la comparaison des possibilités ouvertes par les différentes méthodes fait partie des attendus du stage.

5. Objectifs détaillés

Le résultat de base attendu est :

• une définition précise des propriétés et hypothèses retenues ;
• un prototype utilisant une approche principale sur un sous-ensemble documenté de FDEVSML ;
• une évaluation sur quelques modèles atomiques ;
• une analyse des résultats et des limites.

Le prototype pourra prendre la forme d’un générateur de code vers un solveur logique ou d’une formalisation dans un assistant de preuve, selon l’approche choisie.

L’extension aux modèles couplés, l’étude de propriétés temporelles supplémentaires et l’intégration complète à FT4DEVS constituent des prolongements possibles. La prise en charge de l’ensemble du langage et de tous les modèles d’exemple n’est pas attendue en six mois.

Le stage est exploratoire : identifier et expliquer une limite d’une méthode constitue aussi un résultat scientifique utile. Une phase d’étude bibliographique conséquente est attendue. Le périmètre sera ajusté avec les encadrants à partir des premiers résultats.

6. Déroulement prévisionnel

Février – mars : Découverte de DEVS et FDEVSML, étude bibliographique, prise en main de l’AST et essais sur des exemples simples. Définition d’un premier périmètre et choix de l’approche principale avec les encadrants.

Avril – mai : Développement du prototype et premières vérifications sur des modèles atomiques. Analyse des erreurs détectées et des difficultés rencontrées.

Juin : Évaluation sur plusieurs exemples de référence. Selon les résultats, approfondissement de la méthode ou extension à une propriété supplémentaire.

Juillet : Consolidation du prototype, synthèse des résultats et rédaction du rapport. Préparation d’une valorisation scientifique avec les encadrants si les résultats le permettent.

7. Profil recherché et apprentissages

Ce stage s’adresse à un·e étudiant·e intéressé·e par la logique, les propriétés formelles, la modélisation et la recherche.

Bases attendues :

• des connaissances en logique, ensembles, raisonnement mathématique et mathématiques discrètes ;
• la capacité à programmer dans au moins un langage et à comprendre des structures de données ;
• une aisance en anglais pour lire des articles et présenter les résultats ;
• de la curiosité, de la rigueur et le goût d’explorer un problème dont la solution n’est pas entièrement connue.

Connaissances utiles, mais non obligatoires :

• méthodes formelles, automates ou sémantique des langages ;
• solveurs SAT/SMT ou assistants de preuve ;
• programmation fonctionnelle ou manipulation d’arbres syntaxiques.

Les apprentissages prévus pendant le stage :

• DEVS, FDEVSML et la chaîne d’outils FT4DEVS ;
• l’outil de vérification ou de preuve retenu ;
• la formulation de propriétés, la conduite d’expériences et l’analyse de résultats scientifiques.

La programmation fait partie du travail : elle servira à traduire des modèles, construire la formalisation ou automatiser les vérifications. L’équilibre entre développement et preuve dépendra de l’approche retenue.

8. Encadrement, livrables et valorisation

Le stage sera co-encadré au LAAS par Clément Foucher, Luiz Villa et Silvano Dal Zilio en collaboration avec le LISIC de l’Université du Littoral-Côte-d’Opale. Un autre stage sera mené en parallèle au LISIC ; l’articulation des travaux entre les stagiaires sera précisée au démarrage.

• Les livrables comprendront :
• le prototype et sa documentation ;
• les propriétés formalisées et leurs hypothèses ;
• les exemples utilisés pour l’évaluation et les résultats obtenus ;
• le rapport de stage.

Une publication pourra être préparée avec les encadrants si les résultats le permettent. La soumission d’un article constitue un objectif de valorisation, distinct du résultat de base attendu du stage.

9. Modalités pratiques et candidature

Lieu : LAAS-CNRS, Toulouse, France.

Durée : six mois, du 1er février au 31 juillet 2027. Si votre calendrier pédagogique diffère, contactez les encadrants pour discuter de la compatibilité des dates.

Gratification : oui, selon les conditions en vigueur.

Candidature : CV et lettre de motivation, via la plateforme des offres du LAAS-CNRS.

Contacts : ; .

Vous pouvez contacter les encadrants pour discuter de l’adéquation de votre formation au sujet, notamment si vous n’avez pas encore suivi de cours spécialisé en méthodes formelles.

Pour découvrir l’environnement du stage

• Projet et chaîne d’outils FT4DEVS.
• Solveur Z3.
• Assistant de preuves ROCQ.

Les références scientifiques détaillées et la spécification FDEVSML serviront de supports à la prise en main du sujet pendant le stage.

Mots-clés : méthodes formelles ; simulation à événements discrets ; DEVS ; FDEVSML ; invariants ; SMT ; Z3 ; Rocq.