Inria et Mitsubishi Electric collaborent pour élaborer la copie numérique d’une chaîne d’assemblage industrielle

Dans une usine automatisée, chaque maillon de la chaîne de fabrication doit prendre en compte une kyrielle de contraintes et satisfaire à quantité d’exigences. Pour s’assurer que la ligne de production les respecte bien, il faut simuler, tester et vérifier chaque composant. Mais que peut-on prouver formellement quand deux composants hétérogènes interagissent ? Par exemple un logiciel et des éléments de mécanique ? Comment peut-on prouver que cet agrégat hybride satisfait à des exigences communes telles qu’un délai minimal de latence ?

Ces questions alimentent de longue date des conversations entre Jean-Pierre Talpin, responsable de l’équipe de recherche TEA au centre Inria Rennes – Bretagne Atlantique et David Mentré, responsable de l’équipe INS au centre de R&D Europe de Mitsubishi Electric (MERCE) situé sur le même campus. Il s’agit de l’une des plus grosses unités de recherche du groupe en dehors du Japon.

“Au fil de ces échanges, MERCE a décidé de financer une thèse, ce qui est notre façon habituelle de procéder quand nous collaborons avec des laboratoires de recherche académique, explique David Mentré. Effectué par Simon Lunel, ce travail visait principalement à produire un théorème de composition qui, étant donné deux composants pour lesquels nous avons les garanties respectives, va automatiquement fournir la garantie d’ensemble.” Comme le fait remarquer Jean-Pierre Talpin, cette thèse sur la compositionnalité de preuves a connu un impact inattendu : “elle a permis une contribution à KeYmaera X, un prouveur de théorèmes open source développé à l’Université Carnegie Mellon, aux États-Unis.”

Avant cela, plusieurs collaborations ponctuelles Inria-MERCE avaient déjà eu lieu.

“Vers 2012, nous avons commencé à travailler avec l’équipe Toccata du centre Inria de Saclay, détaille David Mentré. Ils développent la technologie Why3, un environnement de preuve qui permet de prouver des propriétés avec de nombreux langages. Nous avons aussi financé une thèse commencée en 2014 au sein de l’équipe πr² à Paris.”

Ces événements ont conduit MERCE et Inria à envisager un accord plus générique destiné à faciliter les collaborations point-à-point qui pourraient de nouveau se présenter dans l’avenir. “Fondamentalement, l’accord-cadre aplanit les problèmes habituels que l’on peut rencontrer dans le montage de ce genre de partenariats, à commencer par la répartition de la propriété intellectuelle. Une fois que tout cela est bien codifié et que les règles sont bien établies, il devient beaucoup plus facile pour les scientifiques de nos deux institutions de travailler ensemble. Par exemple, si nous voulons financer une nouvelle thèse, il nous suffit d’agrafer une annexe à l’accord principal.”

Et financer des thèses, il en est justement question. “Dans l’entreprise, il y a énormément de cas d’étude.” Malgré le contexte industriel, “les sujets de thèse peuvent s’avérer très théoriques. Nous laissons aux étudiants une grande liberté dans l’établissement de leur sujet. Nous n’exigeons pas des applications prêtes à l’emploi que nous pourrions transférer vers nos divisions commerciales à court terme ou quoi que ce soit de ce genre. Si nous nous retrouvons avec une recherche très amont, pas de problème. De toute façon, dans un groupe de 140 000 personnes, ces résultats peuvent intéresser beaucoup de gens.” En ce moment, MERCE finance deux thèses. “Stéphane Kastenbaum a démarré la sienne en octobre 2019. Effectuée à nouveau au sein de l’équipe TEA, elle se situe dans le prolongement de celle de Simon Lunel. Simon avait proposé une avancée théorique sur la vérification modulaire. Stéphane cherchera peut-être des résultats plus algorithmiques : comment incorporer les précédents travaux dans un modèle de programmation similaire à celui utilisé par Mitsubishi Electric. L’autre thèse a démarré en décembre 2018. Réalisée par Emily Clement dans l’équipe Sumo, elle porte sur la robustesse aux imprécisions d’horloge dans la vérification d’automates temporisés. Il s’agit une nouvelle fois d’un travail très amont. Nous envisageons par ailleurs de financer une thèse au sein de Gallinette,” une équipe Inria qui travaille sur les assistants de preuve.

“Il convient de mentionner aussi deux autres collaborations en cours avec Inria. Tout d’abord, le chercheur Reiya Noguchi a quitté le Japon pour passer plusieurs années avec nous au centre R&D de Rennes. Un jour par semaine, il se rend chez Inria dans l’équipe Sumo pour travailler sur la vérification d’automates temporisés. La production scientifique est partagée avec trois chercheurs de cette équipe : Nicolas Markey, Thierry Jéron et Ocan Sankur.”

“Ensuite, Mitsubishi Electric est aussi partie prenante dans le projet ProofInUse.” Lancée par Claude Marché, responsable de l’équipe Inria Toccata, et financée initialement par l’Agence nationale pour la recherche, la première version visait à injecter la technologie Why3 dans SPARK, un langage de programmation formellement basé sur le langage Ada et développé par l’entreprise AdaCore.

Un ProofInUse 2.0 se prépare actuellement. Mitsubishi Electric et d’autres entreprises vont en devenir partenaires. Mais construire un consortium à plusieurs membres s’avère plus complexe. La signature va donc demander un moment. Dans l’intervalle et sans attendre, nous avons convenu avec Toccata d’entamer une collaboration de 18 mois. Ce partenariat d’intérim a été possible parce que nous disposons déjà de l’accord cadre MERCE-Inria.

Et quel est le but ultime de tout ce déploiement ?

“La copie numérique de l’usine, résume David Mentré. Les méthodes formelles et la « compositionnalité » de preuves de systèmes cyberphysiques, y compris les systèmes continus, vont nous aider à élaborer un double numérique de l’installation physique pour qu’un jour, nous puissions concevoir et simuler les process, puis, à partir de là, monter une usine physique qui fonctionnera sans problème du premier coup. C’est notre Graal à long terme. Mais avant d’y arriver, il y aura encore quelques thèses…”