Skip to content. | Skip to navigation

Emergences

Lettre d'information n° 49

Image emergences pour impression
Personal tools
You are here: Home 2017 Lettre d'information n° 49 Vérifier l'intégration des composants hétérogènes d'une usine
Document Actions

Vérifier l'intégration des composants hétérogènes d'une usine

Dans une usine automatisée, chaque maillon de la chaîne de fabrication doit satisfaire à une kyrielle d'exigences. Pour s'assurer que toute la chaine de production respecte les règlementations de sûreté et de sécurité, il faut simuler, tester et vérifier chaque composant et son intégration. Mais que peut-on prouver quand deux composants hétérogènes interagissent, par exemple un logiciel et l’architecture qui l’exécute ? Comment peut on prouver que cet agrégat hybride satisfait des exigences communes comme par exemple un délai de latence ? Voilà les questions au cœur d'une collaboration entre le centre Inria Rennes – Bretagne Atlantique et le centre européen de R&D de Mitsubishi Electric, lui aussi implanté dans la capitale bretonne.

Dans une usine automatisée, chaque maillon de la chaîne de fabrication doit satisfaire à une kyrielle d'exigences. Pour s'assurer que toute la chaine de production respecte les règlementations de sûreté et de sécurité, il faut simuler, tester et vérifier chaque composant et son intégration. Mais que peut-on prouver quand deux composants hétérogènes interagissent, par exemple un logiciel et l’architecture qui l’exécute ? Comment peut-on prouver que cet agrégat hybride satisfait des exigences communes comme par exemple un délai de latence ? Voilà les questions au cœur d'une collaboration entre le centre Inria Rennes – Bretagne Atlantique et le centre européen de R&D de Mitsubishi Electric, lui aussi implanté dans la capitale bretonne.

Équipementier d'envergure mondiale, Mitsubishi Electric conçoit des machines outil, des servomoteurs, des commandes numériques, des robots industriels... De quoi fabriquer une usine de A à Z. La conception de ces chaînes de production s'effectue sur ordinateur. Les différents éléments sont assemblés virtuellement via l'interface graphique d'un logiciel qui peut produire le plan, la schématique, les caractéristiques de l'usine et la documentation correspondante.

Mais un problème subsiste. “Cet outil ne permet pas de vérifier a priori que l'usine va bien fonctionner et respecter les exigences,” explique Jean-Pierre Talpin, responsable de TEA, une équipe-projet Inria qui travaille à définir un cadre permettant de raisonner sur la composition dans les systèmes cyber-physiques. Un exemple concret ? “Le délai d’arrêt d’urgence d’un robot. Pour des raisons de sécurité évidentes, on place généralement le robot dans une cage ou dans un environnement clos. Mais si par mégarde quelqu'un ouvre la porte d’accès vers le robot, il faut alors pouvoir garantir son arrêt immédiat. Le temps nécessaire pour que le système physique se mette à l'arrêt à partir de l'instant où l'on perçoit l'événement “ouverture de porte” s'appelle la latence de bout-en-bout.” Pour l'appréhender, “il faut raisonner à la fois sur le logiciel et le matériel du système temps réel, mais aussi sur la physique ou la mécanique de son environnement.

La question qui se pose alors est de savoir “comment faire pour vérifier que deux composants sont compatibles d’un point de vue logique, au niveau temps réel, et au niveau physique ?” Cette interrogation se trouve au cœur de la thèse de doctorat financée par le centre européen de R&D de Mitsubishi Electric dans le cadre d'une Convention Cifre. Mis en place par le ministère de la Recherche, ce dispositif permet à une entreprise de bénéficier d'une aide financière pour recruter un étudiant dont les travaux, encadrés par un laboratoire académique, conduiront à la soutenance d'une thèse.

Logique dynamique différentielle

Menés par Simon Lunel, ces travaux (1) s'appuient sur un formalisme de logique mathématique appelé logique dynamique différentielle (DL). “C'est elle qui répond le mieux à la problématique, résume Jean-Pierre Talpin. Elle permet de spécifier et vérifier un système dynamique grâce au démonstrateur de théorème qui l'implémente. Ce démonstrateur va prouver méthodiquement que la spécification d'un système continu vérifie un invariant différentiel, c'est-à-dire une propriété logique portant sur des variables continues et formalisant l'exigence que l'on souhaite valider.

Pour ces recherches, les scientifiques ont choisi (et enrichi) KeYmaera, un démonstrateur de théorèmes open source développé à l'université Carnegie Mellon. “Nous avons contribué à cet outil en proposant des opérateurs de composition associatifs et commutatifs pour automatiser la preuve d'invariants composés. Si je prouve un invariant “x” pour le composant A et un invariant “y” pour le composant B, alors lorsque je compose A et B, j'ai une méthode automatique pour prouver que AB possède bien les propriétés “x et y”. C'est ce que nous appelons la compositionnalité des preuves.

Au-delà de cette collaboration ponctuelle, Inria et Mitsubishi Electric envisagent désormais de cheminer vers un partenariat de plus grande ampleur. “Nous réfléchissons à un accord cadre. Dans ce contexte, une délégation de l'industriel a rencontré plusieurs de nos équipes de Rennes et Nantes : TEA, Sumo, Celtique, Tamis et Gallinette. Nos collègues du centre R&D de Mitsubishi sont très orientés recherche, ce qui nous permet d'avoir un dialogue d'autant plus direct.

------
Note :

(1) Compositional proofs in dynamic differential logic. S. Lunel, B. Boyer, J.-P. Talpin. International Conference on Applications of Concurrency to System Design (ACSD'17). Springer, 2017.