Projet ANR-15-CE25-0010 – MODMED : MODèles pour la Vérification de Systèmes Cyber-Physiques MEDicaux
Programme : Sciences et technologies logicielles (DS0705) 2015
Année de financement : 2015
Coordinateur du projet : Monsieur Arnaud Clère (MinMaxMedical)
Partenaires : Entreprise autre que TPE ou PME; Laboratoire public; PME
Montant : 550165.0 euros
Date de début : 2015
Durée : 36 mois
Résumé : 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.