MODéliser les traces d’exécution pour rendre les dispositifs MÉDicaux plus sûrs
(Résumé en français du projet MODMED)
Vérifier ces dispositifs dans leur environnement réel de manière simple, fiable, et continue en analysant formellement leurs traces d’exécution
L’industrie des Systèmes Cyber-Physiques
Médicaux (SCPM) a peu adopté les méthodes formelles pour plusieurs
raisons :
- la modélisation complète des SCPM semble inatteignable car leur utilisation finale n'est pas maîtrisée et leurs capteurs ont une perception limitée de l’environnement.
- les méthodes formelles classiques nécessitent un effort important au démarrage du projet.
- les outils proposés sont souvent inadaptés à cette industrie.
Les efforts semblent donc démesurés pour
des bénéfices incertains dans le développement de systèmes qui sont
rarement critiques.
MODMED prône la vérification de
propriétés de traces d’exécution pour répondre à ces défis et propose
des outils limitant l’effort des développeurs. Les bénéfices attendus
pour les SCPM sont :
- Des prérequis et exigences critiques mieux compris par la formalisation des propriétés
- Des tests systèmes plus efficaces avec des prérequis et un verdict automatisés
- Une surveillance sur le marché plus fiable
- Un usage du SCPM par les chirurgiens mieux compris
- Un diagnostic des problèmes récurrents automatisé
L’adoption de ces outils formels dans
l’industrie des SCPM pourrait entraîner une mutation plus large des
pratiques.
Une approche “ciblée” de la formalisation des SCPM basée sur la surveillance de propriétés de traces d’exécution
Un SCPM peut facilement être
instrumenté pour enregistrer des traces de son exécution. L'analyse des
risques imposée permet d’identifier les exigences critiques des SCPM. Le
principal défi reste l’adoption de méthodes formelles par l'industrie.
MODMED permet de vérifier simplement un sous-ensemble pertinent
d'exigences critiques, de manière précise et fiable en surveillant des
propriétés des traces d’exécution.
Le projet s’organise autour de deux
contributions : une librairie C++ de traces structurées pour
instrumenter à faible coût les SCPM (WP2), et un DSL (Domain Specific
Language) pour exprimer des propriétés des SCPM de façon intuitive et
compréhensible pour les ingénieurs (WP1). Le projet comprend la
réalisation d'outils pour le DSL : générateur de moniteurs (WP3) ;
mesure de couverture des propriétés (WP4) ; extraction de parties de
traces pour d'autres outils (WP5).
MODMED dispose de milliers de traces de
chirurgies réelles qui ont été étudiées pour identifier les exigences du
DSL (WP6/D1). Les outils du projet ont été soumis à des industriels pour
le développement de nouveaux SCPM (WP6/D2). Les résultats du projet ont
été présentés dans des conférences académiques et industrielles (WP7)
pour favoriser leur adoption.
Résultats majeurs du projet
La librairie C++ modmedLog permet de
produire des traces analysables sans changer le code, puis de les
améliorer tout en simplifiant le code.
Le langage ParTraP permet d'exprimer de manière
lisible de très nombreuses propriétés mêlant contraintes temporelles,
données d'événements et fonctions Python. Un environnement de
développement complet (avec éditeur syntaxique, interpréteur,
compilateur vers Java) simplifie l'écriture des propriétés et la
compréhension de leurs résultats.
Ces outils sont disponibles en open
source (https://gricad-gitlab.univ-grenoble-alpes.fr/modmed)
et ont reçu un accueil encourageant d’un panel de développeurs de SCPM.
Production scientifique et brevets
"Requirements for a trace property
language for medical devices" a introduit notre approche formelle légère
à la conférence "Software Engineering in Healthcare Systems" en Suède. ⟨10.1145/3194696.3194699⟩.
⟨hal-02004396⟩
Notre proposition "Enhancing qDebug()"
donnée au Qt Contributors Summit à Berlin nous a conduit à modifier
modmedLog pour atteindre des performances comparables aux librairies
système de traçage. (slides)
"Extending Specification Patterns for
Verification of Parametric Traces" présente nos résultats académiques
dans les minutes de la 6e Intl Conference on Formal Methods in Software
Engineering. ⟨10.1145/3193992.3193998⟩.
⟨hal-02004378⟩
"An Environment for the ParTraP Trace
Property Language" présente les outils de ParTraP et a donné lieu à une
démonstration à la conférence RV 2018 qui réunit la communauté
scientifique autour de la vérification à l’exécution. ⟨10.1007/978-3-030-03769-7_26⟩.
⟨hal-02004420⟩
Illustration
Dans une approche itérative “Utiliser et
Observer un système pour l’Améliorer”, MODMED permet de 1) Mieux tracer,
sans effort, et 2) Formaliser et Evaluer les exigences critiques pour
quantifier les problèmes.
Informations factuelles
MODMED est un projet de recherche
appliquée privée-publique coordonné par Arnaud Clère de la société
MinMaxMedical qui a réuni le Laboratoire d’Informatique de Grenoble
(équipe VASCO) et le fabricant de dispositifs médicaux Blue Ortho. Le
projet a commencé en Octobre 2015 et duré 42 mois. Il a bénéficié d’une
aide ANR de 550 k€ pour un coût global de l’ordre de 1 200 k€.