Description
Dans cet épisode de Science Num, nous découvrons l’univers des méthodes formelles avec Natalia kushik, maîtresse de conférences à Télécom SudParis. Elle nous explique comment ces techniques rigoureuses aident à vérifier et sécuriser les systèmes critiques, et nous parle de ses collaborations industrielles et académiques.
Hébergé par Ausha. Visitez ausha.co/politique-de-confidentialite pour plus d'informations.
Transcription
Bienvenue dans Science NUM, le podcast de Télécom Sud Paris, grande école publique d'ingénieurs du numérique et qui fait partie de l'Institut Polytechnique de Paris. Je suis Annick Dechenet. Dans ce podcast, je reçois des chercheurs, des chercheuses, pour qu'ils nous éclairent sur leur recherche dans le domaine du numérique, qu'est-ce qu'on cherche dans les laboratoires, qu'est-ce qu'on trouve éventuellement. Aujourd'hui, mon invitée est Nathalia Kouchik, elle est experte en méthode formelle. comprendre avec elle ce que sont ces méthodes formelles et à quoi elles servent. Bonjour Natalia.
Bonjour, bonjour Annick.
On aimerait mieux vous connaître, vous et votre parcours.
Oui, avec plaisir. J'ai obtenu mon doctorat à l'Université d'État de Tomsk en 2013. Après, en 2015, j'ai réjoint Télécommissure de Paris en tant que maître de conférence en informatique. Et enfin, en 2022, j'ai eu mon habilitation à diriger de recherche. de l'Institut Polytechnique de Paris.
Votre domaine de recherche principale, ce sont les méthodes formelles et en particulier les tests basés sur des modèles. Vous pouvez en dire un peu plus ?
Ce type de stratégie de test est généralement appliqué aux systèmes et ou leurs composants qui doivent être soigneusement vérifiés avant leur déploiement. Nous utilisons une telle vérification par exemple dans les systèmes critiques, c'est-à-dire les systèmes où un bug ou une erreur de développement ... peuvent provoquer des conséquences graves pour les humains, pour l'environnement, etc. Prenons comme exemple la thèse de doctorat d'Eric Petersen que j'ai encadrée. Cette thèse a été soutenue en décembre dernier. Ce travail a été consacré à l'émulation et la validation des réseaux de liens dynamiques. C'est une application directe de ce type de réseau et de leurs composants associés, par exemple dans le cadre des communications satellites.
Est-ce que ces recherches sont menées avec des industriels ?
En effet, cette dernière thèse que je viens de citer, elle a été réalisée dans le cadre d'un laboratoire commun entre Airbus et Télécom-Juice de Paris. Ce laboratoire a pour objectif la recherche commune dans le domaine de l'informatique et de l'intelligence artificielle pour les réseaux. Elle a été ouverte à l'initiative de Jamal Zeghlaj, qui m'a invité à participer à cette collaboration, car nos collègues de chez Airbus ont exprimé leurs besoins. de stratégie de validation du réseau.
Ok.
De même, dans le cadre du laboratoire commun avec la PME Bio Networks, nous avons utilisé des méthodes formelles pour vérifier et configurer les chaînes de services par exemple. Ou sinon, nous avons également une collaboration très récente avec Orange dans le domaine des méthodes formelles pour la sécurité, pour les systèmes communicants où nous sommes impliqués avec Philippe Schleuber-Kesier.
Les recherches que vous menez intéressent les industriels, on le comprend grâce aux exemples que vous venez de donner. Est-ce que vous êtes aussi sollicité par les institutions ?
Effectivement, parfois nous sommes invités à rejoindre un consortium d'un projet de recherche où les partenaires industriels viennent vers nous directement en nous exprimant leurs besoins, ce qui a été le cas plusieurs fois. En revanche, en même temps, face aux nouveaux défis de défense et de souveraineté, Nous pouvons également constater de nouvelles opportunités au niveau gouvernemental et de nouveaux appels à projets auxquels nous essayons également de répondre.
Pour aller plus loin, pourquoi a-t-on besoin de plus en plus de certifications formelles ?
C'est une très très bonne question parce qu'on voudrait juste s'assurer du bon fonctionnement de nos composants. La plupart du temps, ce sont les composants logiciels. Pour donner des garanties que notre logiciel fonctionne bien, on a besoin de passer par des modèles formels et des méthodes formelles. plus précisément.
Nathalia, qu'est-ce qui vous passionne dans votre métier ?
Nous recherchons toujours le compromis entre l'exhaustivité et la complexité. C'est-à-dire, d'une part, nous souhaitons maximiser le nombre de défauts que l'on peut détecter par la suite de tests, sans pour autant passer des heures et des années, parfois des mois, à développer une telle suite de tests. Nous cherchons donc à minimiser ce temps tout en maximisant l'exhaustivité. C'est ce compromis qui rend ce sujet très curieux, en tout cas pour moi.
Et pourquoi ?
Parce que ce n'est pas évident. Parce que la nature des problèmes, elle est telle que ce n'est pas souvent le cas qu'on arrive à avoir ce compromis.
Les tests basés sur des modèles se développent depuis plus de 50 ans. Donc aujourd'hui, quelle est l'originalité de votre approche ?
Au départ, il s'agissait simplement des machines classiques. utilisés comme des modèles formels, que nous appelons maintenant les machines à états finis ou les automates. Ce sont des modèles qui changent d'état lorsqu'une entrée est appliquée et qu'une sortie est produite. Donc au début, Ces machines étaient déterministes et donc en fait elles permettaient de modéliser les comportements où la sortie est toujours la même pour la même paire d'états et d'entrées. Effectivement, aujourd'hui, ce modèle n'est plus pratique pour modéliser les systèmes actuels qui sont assez grands, assez complexes. Donc nous avons besoin d'étudier les machines et les modèles non déterministes et ensuite nous avons besoin aussi d'en traduire plusieurs aspects dans ces modèles. Les aspects temporels, les conditions d'exécution d'une transition, ce sont des variables internes, etc. Et donc pour cela, nous devons étudier les problèmes similaires pour générer les suites de tests exhaustives pour les machines et les automates non classiques. Soit les machines étendues, temporisées, leurs compositions, etc. C'est exactement ce que nous faisons dans nos recherches. Ce qui rend nos approches originales, à mon sens.
Est-ce qu'il vous arrive d'obtenir des résultats ? que vous n'attendiez pas par exemple ?
Cela arrive et assez souvent d'ailleurs. Parfois nous obtenons des résultats négatifs. Mais nous sommes toujours en mesure de les partager avec la communauté. Il existe des revues même qui recherchent de tels résultats. Si je peux donner un exemple, dans la communauté des tests de mutation, il existe une notion de mutant équivalent, dont tout le monde essaie de s'en débarrasser. Plus précisément, lors des tests de mutation, tests de mutation, nous essayons d'injecter une erreur ou un bague dans le code et de créer un cas de test ou de vérifier si un cas de test donné détecte cette erreur. Par conséquent, injecter des erreurs conduisant à un comportement équivalent n'est pas intéressant et donc les mutants équivalents ne sont pas appréciés car ces mutants n'apportent aucune valeur lorsqu'il s'agit d'évaluer le taux de couverture des fautes par exemple.
D'accord.
En revanche, Nous avons découvert que ce type de mutant, bien qu'il soit inutile pour les tests, peut être utile pour l'optimisation du code. Car ils expriment un comportement équivalent, mais probablement avec des performances supérieures. Apparemment, nos expériences ont montré que c'était exactement le cas. Et nous avons publié ce résultat dans une des revues de Elsevier.
Et si vous receviez des fonds supplémentaires, qu'est-ce que vous feriez avec plus d'argent ?
j'investirais probablement dans les ressources humaines. Avec plus d'argent, nous aurions probablement un groupe plus grand, ce qui permettrait d'avancer plus vite et par conséquent valoriser nos résultats plus vite également.
Comment vous envisagez la suite de vos travaux de recherche ? À quoi ça va ressembler dans les années à venir ?
L'un des axes qui m'intéresse est celui des méthodes formelles et des tests basés sur des modèles pour la sécurité. La modélisation des... La propriété de sécurité des systèmes de communication et la génération des suites de tests exhaustifs dans ce contexte me semblent très intéressants et très challenging. Donc ça c'est la première chose. La deuxième chose c'est que pour les chercheurs, il reste toujours des problèmes non résolus. Dans mon cas, il y a aussi des problèmes fondamentaux auxquels on n'a pas trouvé de solution, notamment dans le cadre de tests exhaustifs pour les machines à état fini non classique. dont j'espère pouvoir traiter un jour.
Merci Nathalie Akouchik d'avoir accepté de partager vos recherches avec nous et de nous avoir permis de mieux comprendre vos travaux. Je rappelle que Science Nume est un podcast soutenu par le Carnot Télécom et Société Numérique. Si vous êtes intéressé par la recherche dans le domaine du numérique, je vous invite à retrouver tous les épisodes précédents sur vos plateformes d'écoute préférées. A bientôt !
Description
Dans cet épisode de Science Num, nous découvrons l’univers des méthodes formelles avec Natalia kushik, maîtresse de conférences à Télécom SudParis. Elle nous explique comment ces techniques rigoureuses aident à vérifier et sécuriser les systèmes critiques, et nous parle de ses collaborations industrielles et académiques.
Hébergé par Ausha. Visitez ausha.co/politique-de-confidentialite pour plus d'informations.
Transcription
Bienvenue dans Science NUM, le podcast de Télécom Sud Paris, grande école publique d'ingénieurs du numérique et qui fait partie de l'Institut Polytechnique de Paris. Je suis Annick Dechenet. Dans ce podcast, je reçois des chercheurs, des chercheuses, pour qu'ils nous éclairent sur leur recherche dans le domaine du numérique, qu'est-ce qu'on cherche dans les laboratoires, qu'est-ce qu'on trouve éventuellement. Aujourd'hui, mon invitée est Nathalia Kouchik, elle est experte en méthode formelle. comprendre avec elle ce que sont ces méthodes formelles et à quoi elles servent. Bonjour Natalia.
Bonjour, bonjour Annick.
On aimerait mieux vous connaître, vous et votre parcours.
Oui, avec plaisir. J'ai obtenu mon doctorat à l'Université d'État de Tomsk en 2013. Après, en 2015, j'ai réjoint Télécommissure de Paris en tant que maître de conférence en informatique. Et enfin, en 2022, j'ai eu mon habilitation à diriger de recherche. de l'Institut Polytechnique de Paris.
Votre domaine de recherche principale, ce sont les méthodes formelles et en particulier les tests basés sur des modèles. Vous pouvez en dire un peu plus ?
Ce type de stratégie de test est généralement appliqué aux systèmes et ou leurs composants qui doivent être soigneusement vérifiés avant leur déploiement. Nous utilisons une telle vérification par exemple dans les systèmes critiques, c'est-à-dire les systèmes où un bug ou une erreur de développement ... peuvent provoquer des conséquences graves pour les humains, pour l'environnement, etc. Prenons comme exemple la thèse de doctorat d'Eric Petersen que j'ai encadrée. Cette thèse a été soutenue en décembre dernier. Ce travail a été consacré à l'émulation et la validation des réseaux de liens dynamiques. C'est une application directe de ce type de réseau et de leurs composants associés, par exemple dans le cadre des communications satellites.
Est-ce que ces recherches sont menées avec des industriels ?
En effet, cette dernière thèse que je viens de citer, elle a été réalisée dans le cadre d'un laboratoire commun entre Airbus et Télécom-Juice de Paris. Ce laboratoire a pour objectif la recherche commune dans le domaine de l'informatique et de l'intelligence artificielle pour les réseaux. Elle a été ouverte à l'initiative de Jamal Zeghlaj, qui m'a invité à participer à cette collaboration, car nos collègues de chez Airbus ont exprimé leurs besoins. de stratégie de validation du réseau.
Ok.
De même, dans le cadre du laboratoire commun avec la PME Bio Networks, nous avons utilisé des méthodes formelles pour vérifier et configurer les chaînes de services par exemple. Ou sinon, nous avons également une collaboration très récente avec Orange dans le domaine des méthodes formelles pour la sécurité, pour les systèmes communicants où nous sommes impliqués avec Philippe Schleuber-Kesier.
Les recherches que vous menez intéressent les industriels, on le comprend grâce aux exemples que vous venez de donner. Est-ce que vous êtes aussi sollicité par les institutions ?
Effectivement, parfois nous sommes invités à rejoindre un consortium d'un projet de recherche où les partenaires industriels viennent vers nous directement en nous exprimant leurs besoins, ce qui a été le cas plusieurs fois. En revanche, en même temps, face aux nouveaux défis de défense et de souveraineté, Nous pouvons également constater de nouvelles opportunités au niveau gouvernemental et de nouveaux appels à projets auxquels nous essayons également de répondre.
Pour aller plus loin, pourquoi a-t-on besoin de plus en plus de certifications formelles ?
C'est une très très bonne question parce qu'on voudrait juste s'assurer du bon fonctionnement de nos composants. La plupart du temps, ce sont les composants logiciels. Pour donner des garanties que notre logiciel fonctionne bien, on a besoin de passer par des modèles formels et des méthodes formelles. plus précisément.
Nathalia, qu'est-ce qui vous passionne dans votre métier ?
Nous recherchons toujours le compromis entre l'exhaustivité et la complexité. C'est-à-dire, d'une part, nous souhaitons maximiser le nombre de défauts que l'on peut détecter par la suite de tests, sans pour autant passer des heures et des années, parfois des mois, à développer une telle suite de tests. Nous cherchons donc à minimiser ce temps tout en maximisant l'exhaustivité. C'est ce compromis qui rend ce sujet très curieux, en tout cas pour moi.
Et pourquoi ?
Parce que ce n'est pas évident. Parce que la nature des problèmes, elle est telle que ce n'est pas souvent le cas qu'on arrive à avoir ce compromis.
Les tests basés sur des modèles se développent depuis plus de 50 ans. Donc aujourd'hui, quelle est l'originalité de votre approche ?
Au départ, il s'agissait simplement des machines classiques. utilisés comme des modèles formels, que nous appelons maintenant les machines à états finis ou les automates. Ce sont des modèles qui changent d'état lorsqu'une entrée est appliquée et qu'une sortie est produite. Donc au début, Ces machines étaient déterministes et donc en fait elles permettaient de modéliser les comportements où la sortie est toujours la même pour la même paire d'états et d'entrées. Effectivement, aujourd'hui, ce modèle n'est plus pratique pour modéliser les systèmes actuels qui sont assez grands, assez complexes. Donc nous avons besoin d'étudier les machines et les modèles non déterministes et ensuite nous avons besoin aussi d'en traduire plusieurs aspects dans ces modèles. Les aspects temporels, les conditions d'exécution d'une transition, ce sont des variables internes, etc. Et donc pour cela, nous devons étudier les problèmes similaires pour générer les suites de tests exhaustives pour les machines et les automates non classiques. Soit les machines étendues, temporisées, leurs compositions, etc. C'est exactement ce que nous faisons dans nos recherches. Ce qui rend nos approches originales, à mon sens.
Est-ce qu'il vous arrive d'obtenir des résultats ? que vous n'attendiez pas par exemple ?
Cela arrive et assez souvent d'ailleurs. Parfois nous obtenons des résultats négatifs. Mais nous sommes toujours en mesure de les partager avec la communauté. Il existe des revues même qui recherchent de tels résultats. Si je peux donner un exemple, dans la communauté des tests de mutation, il existe une notion de mutant équivalent, dont tout le monde essaie de s'en débarrasser. Plus précisément, lors des tests de mutation, tests de mutation, nous essayons d'injecter une erreur ou un bague dans le code et de créer un cas de test ou de vérifier si un cas de test donné détecte cette erreur. Par conséquent, injecter des erreurs conduisant à un comportement équivalent n'est pas intéressant et donc les mutants équivalents ne sont pas appréciés car ces mutants n'apportent aucune valeur lorsqu'il s'agit d'évaluer le taux de couverture des fautes par exemple.
D'accord.
En revanche, Nous avons découvert que ce type de mutant, bien qu'il soit inutile pour les tests, peut être utile pour l'optimisation du code. Car ils expriment un comportement équivalent, mais probablement avec des performances supérieures. Apparemment, nos expériences ont montré que c'était exactement le cas. Et nous avons publié ce résultat dans une des revues de Elsevier.
Et si vous receviez des fonds supplémentaires, qu'est-ce que vous feriez avec plus d'argent ?
j'investirais probablement dans les ressources humaines. Avec plus d'argent, nous aurions probablement un groupe plus grand, ce qui permettrait d'avancer plus vite et par conséquent valoriser nos résultats plus vite également.
Comment vous envisagez la suite de vos travaux de recherche ? À quoi ça va ressembler dans les années à venir ?
L'un des axes qui m'intéresse est celui des méthodes formelles et des tests basés sur des modèles pour la sécurité. La modélisation des... La propriété de sécurité des systèmes de communication et la génération des suites de tests exhaustifs dans ce contexte me semblent très intéressants et très challenging. Donc ça c'est la première chose. La deuxième chose c'est que pour les chercheurs, il reste toujours des problèmes non résolus. Dans mon cas, il y a aussi des problèmes fondamentaux auxquels on n'a pas trouvé de solution, notamment dans le cadre de tests exhaustifs pour les machines à état fini non classique. dont j'espère pouvoir traiter un jour.
Merci Nathalie Akouchik d'avoir accepté de partager vos recherches avec nous et de nous avoir permis de mieux comprendre vos travaux. Je rappelle que Science Nume est un podcast soutenu par le Carnot Télécom et Société Numérique. Si vous êtes intéressé par la recherche dans le domaine du numérique, je vous invite à retrouver tous les épisodes précédents sur vos plateformes d'écoute préférées. A bientôt !
Share
Embed
You may also like
Description
Dans cet épisode de Science Num, nous découvrons l’univers des méthodes formelles avec Natalia kushik, maîtresse de conférences à Télécom SudParis. Elle nous explique comment ces techniques rigoureuses aident à vérifier et sécuriser les systèmes critiques, et nous parle de ses collaborations industrielles et académiques.
Hébergé par Ausha. Visitez ausha.co/politique-de-confidentialite pour plus d'informations.
Transcription
Bienvenue dans Science NUM, le podcast de Télécom Sud Paris, grande école publique d'ingénieurs du numérique et qui fait partie de l'Institut Polytechnique de Paris. Je suis Annick Dechenet. Dans ce podcast, je reçois des chercheurs, des chercheuses, pour qu'ils nous éclairent sur leur recherche dans le domaine du numérique, qu'est-ce qu'on cherche dans les laboratoires, qu'est-ce qu'on trouve éventuellement. Aujourd'hui, mon invitée est Nathalia Kouchik, elle est experte en méthode formelle. comprendre avec elle ce que sont ces méthodes formelles et à quoi elles servent. Bonjour Natalia.
Bonjour, bonjour Annick.
On aimerait mieux vous connaître, vous et votre parcours.
Oui, avec plaisir. J'ai obtenu mon doctorat à l'Université d'État de Tomsk en 2013. Après, en 2015, j'ai réjoint Télécommissure de Paris en tant que maître de conférence en informatique. Et enfin, en 2022, j'ai eu mon habilitation à diriger de recherche. de l'Institut Polytechnique de Paris.
Votre domaine de recherche principale, ce sont les méthodes formelles et en particulier les tests basés sur des modèles. Vous pouvez en dire un peu plus ?
Ce type de stratégie de test est généralement appliqué aux systèmes et ou leurs composants qui doivent être soigneusement vérifiés avant leur déploiement. Nous utilisons une telle vérification par exemple dans les systèmes critiques, c'est-à-dire les systèmes où un bug ou une erreur de développement ... peuvent provoquer des conséquences graves pour les humains, pour l'environnement, etc. Prenons comme exemple la thèse de doctorat d'Eric Petersen que j'ai encadrée. Cette thèse a été soutenue en décembre dernier. Ce travail a été consacré à l'émulation et la validation des réseaux de liens dynamiques. C'est une application directe de ce type de réseau et de leurs composants associés, par exemple dans le cadre des communications satellites.
Est-ce que ces recherches sont menées avec des industriels ?
En effet, cette dernière thèse que je viens de citer, elle a été réalisée dans le cadre d'un laboratoire commun entre Airbus et Télécom-Juice de Paris. Ce laboratoire a pour objectif la recherche commune dans le domaine de l'informatique et de l'intelligence artificielle pour les réseaux. Elle a été ouverte à l'initiative de Jamal Zeghlaj, qui m'a invité à participer à cette collaboration, car nos collègues de chez Airbus ont exprimé leurs besoins. de stratégie de validation du réseau.
Ok.
De même, dans le cadre du laboratoire commun avec la PME Bio Networks, nous avons utilisé des méthodes formelles pour vérifier et configurer les chaînes de services par exemple. Ou sinon, nous avons également une collaboration très récente avec Orange dans le domaine des méthodes formelles pour la sécurité, pour les systèmes communicants où nous sommes impliqués avec Philippe Schleuber-Kesier.
Les recherches que vous menez intéressent les industriels, on le comprend grâce aux exemples que vous venez de donner. Est-ce que vous êtes aussi sollicité par les institutions ?
Effectivement, parfois nous sommes invités à rejoindre un consortium d'un projet de recherche où les partenaires industriels viennent vers nous directement en nous exprimant leurs besoins, ce qui a été le cas plusieurs fois. En revanche, en même temps, face aux nouveaux défis de défense et de souveraineté, Nous pouvons également constater de nouvelles opportunités au niveau gouvernemental et de nouveaux appels à projets auxquels nous essayons également de répondre.
Pour aller plus loin, pourquoi a-t-on besoin de plus en plus de certifications formelles ?
C'est une très très bonne question parce qu'on voudrait juste s'assurer du bon fonctionnement de nos composants. La plupart du temps, ce sont les composants logiciels. Pour donner des garanties que notre logiciel fonctionne bien, on a besoin de passer par des modèles formels et des méthodes formelles. plus précisément.
Nathalia, qu'est-ce qui vous passionne dans votre métier ?
Nous recherchons toujours le compromis entre l'exhaustivité et la complexité. C'est-à-dire, d'une part, nous souhaitons maximiser le nombre de défauts que l'on peut détecter par la suite de tests, sans pour autant passer des heures et des années, parfois des mois, à développer une telle suite de tests. Nous cherchons donc à minimiser ce temps tout en maximisant l'exhaustivité. C'est ce compromis qui rend ce sujet très curieux, en tout cas pour moi.
Et pourquoi ?
Parce que ce n'est pas évident. Parce que la nature des problèmes, elle est telle que ce n'est pas souvent le cas qu'on arrive à avoir ce compromis.
Les tests basés sur des modèles se développent depuis plus de 50 ans. Donc aujourd'hui, quelle est l'originalité de votre approche ?
Au départ, il s'agissait simplement des machines classiques. utilisés comme des modèles formels, que nous appelons maintenant les machines à états finis ou les automates. Ce sont des modèles qui changent d'état lorsqu'une entrée est appliquée et qu'une sortie est produite. Donc au début, Ces machines étaient déterministes et donc en fait elles permettaient de modéliser les comportements où la sortie est toujours la même pour la même paire d'états et d'entrées. Effectivement, aujourd'hui, ce modèle n'est plus pratique pour modéliser les systèmes actuels qui sont assez grands, assez complexes. Donc nous avons besoin d'étudier les machines et les modèles non déterministes et ensuite nous avons besoin aussi d'en traduire plusieurs aspects dans ces modèles. Les aspects temporels, les conditions d'exécution d'une transition, ce sont des variables internes, etc. Et donc pour cela, nous devons étudier les problèmes similaires pour générer les suites de tests exhaustives pour les machines et les automates non classiques. Soit les machines étendues, temporisées, leurs compositions, etc. C'est exactement ce que nous faisons dans nos recherches. Ce qui rend nos approches originales, à mon sens.
Est-ce qu'il vous arrive d'obtenir des résultats ? que vous n'attendiez pas par exemple ?
Cela arrive et assez souvent d'ailleurs. Parfois nous obtenons des résultats négatifs. Mais nous sommes toujours en mesure de les partager avec la communauté. Il existe des revues même qui recherchent de tels résultats. Si je peux donner un exemple, dans la communauté des tests de mutation, il existe une notion de mutant équivalent, dont tout le monde essaie de s'en débarrasser. Plus précisément, lors des tests de mutation, tests de mutation, nous essayons d'injecter une erreur ou un bague dans le code et de créer un cas de test ou de vérifier si un cas de test donné détecte cette erreur. Par conséquent, injecter des erreurs conduisant à un comportement équivalent n'est pas intéressant et donc les mutants équivalents ne sont pas appréciés car ces mutants n'apportent aucune valeur lorsqu'il s'agit d'évaluer le taux de couverture des fautes par exemple.
D'accord.
En revanche, Nous avons découvert que ce type de mutant, bien qu'il soit inutile pour les tests, peut être utile pour l'optimisation du code. Car ils expriment un comportement équivalent, mais probablement avec des performances supérieures. Apparemment, nos expériences ont montré que c'était exactement le cas. Et nous avons publié ce résultat dans une des revues de Elsevier.
Et si vous receviez des fonds supplémentaires, qu'est-ce que vous feriez avec plus d'argent ?
j'investirais probablement dans les ressources humaines. Avec plus d'argent, nous aurions probablement un groupe plus grand, ce qui permettrait d'avancer plus vite et par conséquent valoriser nos résultats plus vite également.
Comment vous envisagez la suite de vos travaux de recherche ? À quoi ça va ressembler dans les années à venir ?
L'un des axes qui m'intéresse est celui des méthodes formelles et des tests basés sur des modèles pour la sécurité. La modélisation des... La propriété de sécurité des systèmes de communication et la génération des suites de tests exhaustifs dans ce contexte me semblent très intéressants et très challenging. Donc ça c'est la première chose. La deuxième chose c'est que pour les chercheurs, il reste toujours des problèmes non résolus. Dans mon cas, il y a aussi des problèmes fondamentaux auxquels on n'a pas trouvé de solution, notamment dans le cadre de tests exhaustifs pour les machines à état fini non classique. dont j'espère pouvoir traiter un jour.
Merci Nathalie Akouchik d'avoir accepté de partager vos recherches avec nous et de nous avoir permis de mieux comprendre vos travaux. Je rappelle que Science Nume est un podcast soutenu par le Carnot Télécom et Société Numérique. Si vous êtes intéressé par la recherche dans le domaine du numérique, je vous invite à retrouver tous les épisodes précédents sur vos plateformes d'écoute préférées. A bientôt !
Description
Dans cet épisode de Science Num, nous découvrons l’univers des méthodes formelles avec Natalia kushik, maîtresse de conférences à Télécom SudParis. Elle nous explique comment ces techniques rigoureuses aident à vérifier et sécuriser les systèmes critiques, et nous parle de ses collaborations industrielles et académiques.
Hébergé par Ausha. Visitez ausha.co/politique-de-confidentialite pour plus d'informations.
Transcription
Bienvenue dans Science NUM, le podcast de Télécom Sud Paris, grande école publique d'ingénieurs du numérique et qui fait partie de l'Institut Polytechnique de Paris. Je suis Annick Dechenet. Dans ce podcast, je reçois des chercheurs, des chercheuses, pour qu'ils nous éclairent sur leur recherche dans le domaine du numérique, qu'est-ce qu'on cherche dans les laboratoires, qu'est-ce qu'on trouve éventuellement. Aujourd'hui, mon invitée est Nathalia Kouchik, elle est experte en méthode formelle. comprendre avec elle ce que sont ces méthodes formelles et à quoi elles servent. Bonjour Natalia.
Bonjour, bonjour Annick.
On aimerait mieux vous connaître, vous et votre parcours.
Oui, avec plaisir. J'ai obtenu mon doctorat à l'Université d'État de Tomsk en 2013. Après, en 2015, j'ai réjoint Télécommissure de Paris en tant que maître de conférence en informatique. Et enfin, en 2022, j'ai eu mon habilitation à diriger de recherche. de l'Institut Polytechnique de Paris.
Votre domaine de recherche principale, ce sont les méthodes formelles et en particulier les tests basés sur des modèles. Vous pouvez en dire un peu plus ?
Ce type de stratégie de test est généralement appliqué aux systèmes et ou leurs composants qui doivent être soigneusement vérifiés avant leur déploiement. Nous utilisons une telle vérification par exemple dans les systèmes critiques, c'est-à-dire les systèmes où un bug ou une erreur de développement ... peuvent provoquer des conséquences graves pour les humains, pour l'environnement, etc. Prenons comme exemple la thèse de doctorat d'Eric Petersen que j'ai encadrée. Cette thèse a été soutenue en décembre dernier. Ce travail a été consacré à l'émulation et la validation des réseaux de liens dynamiques. C'est une application directe de ce type de réseau et de leurs composants associés, par exemple dans le cadre des communications satellites.
Est-ce que ces recherches sont menées avec des industriels ?
En effet, cette dernière thèse que je viens de citer, elle a été réalisée dans le cadre d'un laboratoire commun entre Airbus et Télécom-Juice de Paris. Ce laboratoire a pour objectif la recherche commune dans le domaine de l'informatique et de l'intelligence artificielle pour les réseaux. Elle a été ouverte à l'initiative de Jamal Zeghlaj, qui m'a invité à participer à cette collaboration, car nos collègues de chez Airbus ont exprimé leurs besoins. de stratégie de validation du réseau.
Ok.
De même, dans le cadre du laboratoire commun avec la PME Bio Networks, nous avons utilisé des méthodes formelles pour vérifier et configurer les chaînes de services par exemple. Ou sinon, nous avons également une collaboration très récente avec Orange dans le domaine des méthodes formelles pour la sécurité, pour les systèmes communicants où nous sommes impliqués avec Philippe Schleuber-Kesier.
Les recherches que vous menez intéressent les industriels, on le comprend grâce aux exemples que vous venez de donner. Est-ce que vous êtes aussi sollicité par les institutions ?
Effectivement, parfois nous sommes invités à rejoindre un consortium d'un projet de recherche où les partenaires industriels viennent vers nous directement en nous exprimant leurs besoins, ce qui a été le cas plusieurs fois. En revanche, en même temps, face aux nouveaux défis de défense et de souveraineté, Nous pouvons également constater de nouvelles opportunités au niveau gouvernemental et de nouveaux appels à projets auxquels nous essayons également de répondre.
Pour aller plus loin, pourquoi a-t-on besoin de plus en plus de certifications formelles ?
C'est une très très bonne question parce qu'on voudrait juste s'assurer du bon fonctionnement de nos composants. La plupart du temps, ce sont les composants logiciels. Pour donner des garanties que notre logiciel fonctionne bien, on a besoin de passer par des modèles formels et des méthodes formelles. plus précisément.
Nathalia, qu'est-ce qui vous passionne dans votre métier ?
Nous recherchons toujours le compromis entre l'exhaustivité et la complexité. C'est-à-dire, d'une part, nous souhaitons maximiser le nombre de défauts que l'on peut détecter par la suite de tests, sans pour autant passer des heures et des années, parfois des mois, à développer une telle suite de tests. Nous cherchons donc à minimiser ce temps tout en maximisant l'exhaustivité. C'est ce compromis qui rend ce sujet très curieux, en tout cas pour moi.
Et pourquoi ?
Parce que ce n'est pas évident. Parce que la nature des problèmes, elle est telle que ce n'est pas souvent le cas qu'on arrive à avoir ce compromis.
Les tests basés sur des modèles se développent depuis plus de 50 ans. Donc aujourd'hui, quelle est l'originalité de votre approche ?
Au départ, il s'agissait simplement des machines classiques. utilisés comme des modèles formels, que nous appelons maintenant les machines à états finis ou les automates. Ce sont des modèles qui changent d'état lorsqu'une entrée est appliquée et qu'une sortie est produite. Donc au début, Ces machines étaient déterministes et donc en fait elles permettaient de modéliser les comportements où la sortie est toujours la même pour la même paire d'états et d'entrées. Effectivement, aujourd'hui, ce modèle n'est plus pratique pour modéliser les systèmes actuels qui sont assez grands, assez complexes. Donc nous avons besoin d'étudier les machines et les modèles non déterministes et ensuite nous avons besoin aussi d'en traduire plusieurs aspects dans ces modèles. Les aspects temporels, les conditions d'exécution d'une transition, ce sont des variables internes, etc. Et donc pour cela, nous devons étudier les problèmes similaires pour générer les suites de tests exhaustives pour les machines et les automates non classiques. Soit les machines étendues, temporisées, leurs compositions, etc. C'est exactement ce que nous faisons dans nos recherches. Ce qui rend nos approches originales, à mon sens.
Est-ce qu'il vous arrive d'obtenir des résultats ? que vous n'attendiez pas par exemple ?
Cela arrive et assez souvent d'ailleurs. Parfois nous obtenons des résultats négatifs. Mais nous sommes toujours en mesure de les partager avec la communauté. Il existe des revues même qui recherchent de tels résultats. Si je peux donner un exemple, dans la communauté des tests de mutation, il existe une notion de mutant équivalent, dont tout le monde essaie de s'en débarrasser. Plus précisément, lors des tests de mutation, tests de mutation, nous essayons d'injecter une erreur ou un bague dans le code et de créer un cas de test ou de vérifier si un cas de test donné détecte cette erreur. Par conséquent, injecter des erreurs conduisant à un comportement équivalent n'est pas intéressant et donc les mutants équivalents ne sont pas appréciés car ces mutants n'apportent aucune valeur lorsqu'il s'agit d'évaluer le taux de couverture des fautes par exemple.
D'accord.
En revanche, Nous avons découvert que ce type de mutant, bien qu'il soit inutile pour les tests, peut être utile pour l'optimisation du code. Car ils expriment un comportement équivalent, mais probablement avec des performances supérieures. Apparemment, nos expériences ont montré que c'était exactement le cas. Et nous avons publié ce résultat dans une des revues de Elsevier.
Et si vous receviez des fonds supplémentaires, qu'est-ce que vous feriez avec plus d'argent ?
j'investirais probablement dans les ressources humaines. Avec plus d'argent, nous aurions probablement un groupe plus grand, ce qui permettrait d'avancer plus vite et par conséquent valoriser nos résultats plus vite également.
Comment vous envisagez la suite de vos travaux de recherche ? À quoi ça va ressembler dans les années à venir ?
L'un des axes qui m'intéresse est celui des méthodes formelles et des tests basés sur des modèles pour la sécurité. La modélisation des... La propriété de sécurité des systèmes de communication et la génération des suites de tests exhaustifs dans ce contexte me semblent très intéressants et très challenging. Donc ça c'est la première chose. La deuxième chose c'est que pour les chercheurs, il reste toujours des problèmes non résolus. Dans mon cas, il y a aussi des problèmes fondamentaux auxquels on n'a pas trouvé de solution, notamment dans le cadre de tests exhaustifs pour les machines à état fini non classique. dont j'espère pouvoir traiter un jour.
Merci Nathalie Akouchik d'avoir accepté de partager vos recherches avec nous et de nous avoir permis de mieux comprendre vos travaux. Je rappelle que Science Nume est un podcast soutenu par le Carnot Télécom et Société Numérique. Si vous êtes intéressé par la recherche dans le domaine du numérique, je vous invite à retrouver tous les épisodes précédents sur vos plateformes d'écoute préférées. A bientôt !
Share
Embed
You may also like