MODèles pour la Vérification de Systèmes Cyber-Physiques MEDicaux – MODMED

Un SCPM peut facilement être instrumenté pour enregistrer des traces de son exécution. Celles-ci permettent de comprendre comment il se comporte et est utilisé. L’analyse de risques imposée à ce type de projets permet d’identifier les exigences critiques des SCPM. C’est pourquoi MODMED s’intéresse à une vérification partielle basée sur la surveillance de propriétés de ces traces d’exécution.

Le projet s’organise autour de deux contributions : une librairie C++ de traces structurées, qui insère des instructions de traçage dans les logiciels, et un DSL (Domain Specific Language) qui exprime les propriétés des traces. Le principal défi est l’adoption de ces technologies par les ingénieurs logiciels : l’insertion à faible coût de points de traces doit y enregistrer une information complète, cohérente et structurée ; le DSL doit pouvoir exprimer les principales propriétés des SCPM de façon intuitive et compréhensible pour les ingénieurs.

L’organisation du projet MODMED comprend la définition du DSL pour la spécification d’exigences des SCPM (WP1) et la réalisation de son outillage : générateur de moniteurs (WP3) et mesure de couverture des propriétés (WP4). Cet outillage s’appuie sur une librairie de traces structurées (WP2) pour l’instrumentation de logiciels C++ pour les SCPM. D’autres outils exploitent le corpus de traces pour mieux les comprendre (WP5). A cette fin, le projet dispose de milliers de traces de chirurgies réelles. Celles-ci ont été étudiées pour identifier les exigences du DSL (WP6/D1). En outre, les outils du projet seront expérimentés lors du développement d’un nouveau SCPM (WP6/D2). Enfin, les résultats du projet seront présentés dans des conférences académiques et industrielles (WP7) pour favoriser leur adoption.

La première partie du projet MODMED fut dédiée à l’identification des besoins pour le DSL et la librairie de traces (WP6/D1), à une première définition du DSL (WP1/D1), à la réalisation de deux versions de la librairie de traces (WP2/D1) et d’un prototype de moniteur pour le DSL (WP3/D1).

L’analyse des besoins a étudié le produit TKA de Blue Ortho. TKA (Total Knee Arthroplasty) est un système d’aide à la pose de la prothèse du genou utilisé dans le monde entier. 7000 traces d’opérations ont été collectées par Blue Ortho. Ces traces enregistrent les données des capteurs et les interactions avec le chirurgien et ont été utilisées par le projet MODMED pour la définition du DSL.
Les partenaires du projet ont consacré 15 réunions à comprendre TKA en profondeur (présentations, session pratique, revue de documentation, étude de traces). Ils ont ainsi sélectionné 15 propriétés représentatives de ce qu’il faut vérifier sur les traces. Ces propriétés expriment les exigences pour le SCPM, mais aussi des hypothèses sur son environnement ou l’usage qui en sera fait. Ces hypothèses et propriétés d’usage doivent être évaluées sur les traces de chirurgies réelles.

Une première version du DSL a été définie, sur base de ces propriétés, et implantée. Vis à vis de ses concurrents, ce DSL met l’accent sur l’utilisabilité. Il exprime des propriétés temporelles entre plusieurs événements paramétrés. Il permet l’appel à des prédicats externes pour exprimer des propriétés géométriques ou d’IHM en python ou C++. Enfin, contrairement à ce que nous avions anticipé, les propriétés de TKA font rarement appel au temps réel.

De plus, une librairie C++ de traces structurées a été progressivement améliorée pour structurer les traces sans changer le code existant. Les traces pouvant être améliorées en simplifiant les points de trace et en définissant une fonction par type de données tracé.

Ces outils ont reçu un accueil encourageant d’un panel d’utilisateurs potentiels, développeurs de SCPM.

La première partie du projet a été principalement consacrée à l’analyse des besoins et à la compréhension des spécificités du SCPM TKA. Cette étude nous fournit une base solide pour les contributions du projet MODMED. Une première version du DSL, un prototype d’outil de monitoring et deux versions de la librairie de traces ont été réalisés.

La suite du projet comprend les tâches suivantes:
- Définir des mesures de couverture des propriétés (WP4) pour identifier quelles facettes d’une propriété sont mises en oeuvre par une trace ou un ensemble de traces. Cette étude nous permet de mieux cerner la sémantique du langage de propriétés. L’outillage associé aidera à identifier un ensemble de tests diversifiés pour une propriété donnée.
- Etudier les propriétés d’un grand ensemble de traces (WP5). Notre DSL, conçu pour exprimer des propriétés d’une seule trace, peut être adapté pour sélectionner toutes les traces satisfaisant une propriété donnée, ou pour extraire de ces traces des valeurs de certains paramètres pour un traitement statistique.
- Construire un outillage intégré pour le DSL, qui facilitera l’expression de propriétés, leur évaluation sur une trace, et l’explication du résultat obtenu.
- Approfondir la sémantique du DSL, et les fonctionnalités de la librairie de traces sur base des retours sur les premières versions.
- Présenter le DSL et son outillage dans des conférences scientifiques et industrielles.
- Proposer une taxonomie spécifique aux SCPM pour faciliter et standardiser l’insertion de points de trace.
- Plaider pour l’utilisation de librairies de traces structurées auprès des communautés du Génie Logiciel.

La première partie du projet était principalement consacrée à l’analyse des besoins. La production scientifique qui en découle est la suivante :
- Un article court, décrivant cette analyse des besoins, a été publié à la conférence AFADL 2016 :
Yoann Blein, Identification de propriétés pour la validation d’un système cyber-physique médical, Actes de AFADL 2016, pages 8-10, Besançon, juin 2016.
- Trois articles (conférences RV 2017, QRS 2017- session industrielle, Qt World Summit 2017) et un poster (Journées du GDR GPL 2017) sont en cours de soumission.
- Un prototype de l’outil de monitoring a été publié comme outil open source, sur la forge du projet ( forge.imag.fr/projects/modmed ), ainsi que deux versions de la librairie C++ de traces structurées.

Pour faciliter des interventions médicales toujours plus complexes, de nouveaux dispositifs médicaux baptisés Systèmes Cyber-Physiques Médicaux (SCPM) utilisent images médicales et capteurs pour aider les médecins, tout comme un système de gestion de vol aide un pilote d’avion. Par exemple, le SCPM de Blue Ortho étudié par MODMED permet de poser plus précisément les Prothèses Totales de Genou, avec l’espoir de diviser le nombre de révisions par deux.

Hélas, contrairement aux industries les plus critiques (spatial, etc.), l’industrie des SCPM rechigne à utiliser des méthodes formelles. Le récent “Pacemaker Challenge” a montré qu’il est théoriquement possible de vérifier complètement certains dispositifs médicaux, mais les SCPM étudiés par MODMED sont utilisés dans des conditions si variées que leur vérification formelle complète semble trop coûteuse. Nous pensons que c’est le cas de beaucoup d’applications, et cherchons à adapter les méthodes formelles pour qu’elles soient adoptées pour les SCPM et dans d’autres industries.

Heureusement, les SCPM peuvent facilement être instrumentés pour fournir des traces d’exécution permettant de comprendre leur utilisation et leur comportement sur le terrain. De plus, l’analyse de risque obligatoirement effectuée par les ingénieurs qualité permet d’identifier des exigences critiques difficiles à vérifier par le test. MODMED se concentre donc sur la vérification partielle de traces d’exécution basée sur des modèles et cherche à mesurer son efficacité pour l’industrie. La conversion des ingénieurs logiciels des SCPM aux méthodes formelles serait un succès particulièrement visible pour convertir d’autres industries du logiciel, avec un impact majeur et durable !

Le consortium MODMED est une opportunité rare de réaliser cet objectif: un fabricant de dispositif médical (Blue Ortho), un laboratoire de recherche (LIG), et un fournisseur de composants logiciels et de services (MinMaxMedical), tous situés à Grenoble, avec le support du pôle de compétitivité Minalogic.

MODMED propose des avancées dans le domaine des langages de spécification de trace, des tests, et du monitoring, et les adapte aux SCPM. Il répond au défi i) de rendre ces exigences formelles manipulables par les ingénieurs logiciels sans formation préalable et lisibles par les experts du domaine, et ii) d’améliorer les outils pour traiter les traces des SCPM. Par exemple, la Logique Temporelle Linéaire a récemment été appliquée à la vérification de Modèles d’Interaction et Présentation (MIP) d’une pompe à perfusion de 14 états mais le MIP du SCPM étudié en comprend plus d’un millier.

Le programme du projet MODMED est de définir un langage dédié à la formalisation des exigences (WP1) et des outils connexes: génération de moniteurs (WP3), évaluation de la qualité des tests (WP4). Ils se baseront sur le développement d’une librairie de trace (WP2) pour instrumenter les programmes C++ des SCPM. D’autres outils analyseront un corpus de traces existantes pour comprendre les traces et en inférer des modèles (WP5). Un SCPM utilisé lors de milliers de chirurgies fournira des exigences pour le DSL et des traces pour les outils (WP6/D1). Le développement d’un nouveau SCPM permettra d’évaluer ces outils (WP6/D2). L’adoption de ces Méthodes Formelles légères par d’autres, sera encouragée par la présentation des résultats de MODMED à des conférences académiques et industrielles (WP7).

Les résultats scientifiques comprendront un langage basé sur une extension des « Quantified Event Automata », et les algorithmes de synthèse de moniteur associés, des mesures de couverture de test, des analyses de trace et inférences de modèles. Les logiciels seront libres. La librairie de trace sera proposée pour inclusion dans la librairie préférée pour développer des systèmes embarqués : Qt. Une librairie commerciale sera développée indépendamment par MinMaxMedical et utilisée dans une douzaine de SCPM conçus par ses partenaires Français.