The French National Research Agency Projects for science

Voir cette page en français

ANR funded project

Sciences et technologies logicielles (DS0705) 2015

MODel-Based Verification of MEDical Cyber-Physical Systems

To support increasingly more complex medical procedures, new medical devices called Medical Cyber-Physical Systems (MCPS) use medical images and sensor data to assist caregivers in the same way Flight Management Systems help a pilot flying planes. For instance, Blue Ortho’s MCPS studied by MODMED allows more precise Total Knee Arthroplasty (i.e. the placement of a femoral and tibial knee prosthesis), potentially dividing the number of revisions by two.

Alas, contrary to the most safety-critical industries (air, space, etc.), the MCPS industry is reluctant to using formal methods. The recent Pacemaker Challenge showed that it is theoretically possible to fully verify some medical devices, but the MCPS studied by MODMED are used in such varied conditions that their full formal verification seems too costly. We suggest this is also true for most industries, and seek to adapt formal methods so they can be adopted in the MCPS and other industries.

Fortunately, MCPS can easily be instrumented to provide execution traces enabling us to understand their use and behaviour in the field. And the risk analysis mandatorily performed by quality engineers is a good point to identify critical MCPS requirements that are difficult to verify by testing. Hence, MODMED will focus on partial Model-Based Verification of execution traces and study how effective it can be. The successful conversion of MCPS software engineers to formal methods would be an important and highly visible milestone to evangelize the broader software engineering community, resulting in a major and lasting impact on the software industry!

The MODMED consortium is a rare opportunity to successfully implement this plan: a medical device manufacturer (Blue Ortho), a research laboratory (LIG), and a software components and services provider (MinMaxMedical), all located in Grenoble with the support of the Minalogic competitiveness cluster.

The MODMED project builds on existing results to propose new advances in the field of trace specification languages, testing and monitoring, and to adapt them to the domain of MCPS. It faces the challenges to i) make formal requirements writable by software engineers with no training in formal methods and readable by domain experts, and ii) scale the tools up to the size of execution traces of MCPS. For instance, Linear Temporal Logic model checking was recently applied to Presentation Interaction Models (PIM) of an infusion pump exhibiting 14 states but the PIM of the studied MCPS has more than a thousand states.

The work programme of the MODMED project is the definition of a Domain Specific Language for specifying MCPS requirements (WP1) and associated tools: monitor generator (WP3), and test assessment (WP4). These will rely on the development of a structured trace library (WP2) allowing to instrument C++ MCPS programs. Additional tools will support further analysis of the corpus of available traces in order to understand them and infer underlying models (WP5). Traces of a real MCPS used in thousands surgeries will first be studied to identify requirements for the DSL (WP6/D1), and the development of a new MCPS will allow evaluating the MODMED toolset (WP6/D2). To encourage the adoption of these lightweight formal methods by other industrials, MODMED results will be presented to academic and industrial conferences (WP7).

The scientific outcomes of the project include a DSL whose semantics is based on an extension of Quantified Event Automata, with associated monitor-synthesis algorithms and test coverage metrics, and the study of trace analysis and model inference tools based on traces. The DSL, tools, and structured trace library will be released as open source software. The trace library will be proposed for inclusion with the #1 one framework for developing cross-platform and embedded systems: Qt. A commercial library will be developed independently by MinMaxMedical for use in a dozen MCPS manufactured by its French partners.



LIG Laboratoire d'Informatique de Grenoble

MMM MinMaxMedical

ANR grant: 550 165 euros
Beginning and duration: octobre 2015 - 36 mois


ANR Programme: Sciences et technologies logicielles (DS0705) 2015

Project ID: ANR-15-CE25-0010

Project coordinator:
Monsieur Arnaud Clère (MinMaxMedical)


Back to the previous page


The project coordinator is the author of this abstract and is therefore responsible for the content of the summary. The ANR disclaims all responsibility in connection with its content.