MODel-Based Verification of MEDical Cyber-Physical Systems – MODMED

MCPS can easily be instrumented to provide execution traces enabling us to understand their use and behaviour in the field. The risk analysis mandatorily performed by quality engineers is a good point to identify critical MCPS requirements. Hence, MODMED focuses on partial Model-Based Verification
of execution traces.

The project is based on two central contributions: a C++ structured trace library which will be used by the developers to insert tracing instructions in their software, and a Domain Specific Language (DSL) to express the expected trace properties. The main challenge of the project is the acceptance of these technologies by the software engineers: insertion of trace points should have minimal cost while providing a complete, consistent and structured information in the traces ; the DSL must be suited to the major properties of MCPS and intuitive enough to allow the expression and understanding of properties by the software engineers.

The work programme of the MODMED project is the definition of a DSL 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 (WP5). Traces and specifications of a real MCPS used in thousands surgeries have been 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 first half of the MODMED project was dedicated to the identification of requirements for the DSL and the trace library (WP6/D1), and then to a first definition of the DSL (WP1/D1), and the development of two versions of the trace library (WP2/D1), and of a prototype monitoring tool for the DSL (WP3/D1).

The requirements study was based on the TKA product of Blue Ortho. TKA is designed to guide Total Knee Arthroplasty surgeries, i.e. the replacement of both tibial and femoral cartilages with implants. This MCPS is used worldwide and has acquired more than 7000 traces of execution, recording events such as sensors acquisitions or interactions with the surgeon. These traces provide a rich raw material for the MODMED DSL.
The partners held about 15 meetings including presentations of the product, a hands-on session, and the review of design documents and sample traces. They reviewed a variety of requirements and listed 15 properties considered representative of what should be verified on the traces. We found that these properties express not only requirements on the TKA MCPS, but also assumptions about its environment and its expected usage which can only be investigated on the deployed system..

Based on these properties, a first version of the DSL was defined and implemented. This DSL is more usable than usual monitoring languages, and supports temporal properties between several parametric events. Further study of the requirements showed that the language should provide a mechanism to call external predicates defined by other means, such as a Python or C++ library, in order to express geometrical or GUI properties. Finally, despite our expectations, the physical time is rarely involved in the properties.

Two versions of the trace library were also released. These tools were informally presented to a panel of prospective users from the MCPS industry. They received positive and encouraging feedback.

The first part of the project has been largely dedicated to the requirements study and the understanding of the TKA MCPS specificities. This study provides a solid basis for the advances of the MODMED project. A first version of the DSL, a prototype monitoring tool, and two releases of the trace library were produced.

The next tasks of the project are as follows:
- Provide coverage metrics (WP4) to measure how much of a property expressed in the DSL has been exercised by a given trace, or a set of traces. This study helps us better understand the semantics of the property language. The associated tool will assist the engineers in the system testing phases to identify a wide variety of test cases.
- Consider properties of a possibly large set of traces (WP5). Although the DSL is designed to express properties on a single trace, it can be adapted to select all traces satisfying a given property, and to retrieve values of parameters from these traces in order to submit these to a statistical analysis.
- Build an integrated environment for the DSL, which will support the expression of properties, their monitoring on a given trace, and explanations of why a property is satisfied or not by the trace.
- Further define the semantics of the DSL, and the capabilities of the trace library, based on the feedback from the first versions.
- Publish the definition of the DSL, and report on its associated toolset in scientific and industrial conferences.
- Define a medical and CPS taxonomy to further help the insertion of trace points while standardizing MCPS traces.
- Advocate the use of structured trace libraries to software engineering communities.

The first half of the project was largely dedicated to the requirements study. The related scientific production is the following:
- A short paper reporting on this requirements study was published at the AFADL 2016 conference :
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.
- Three conference papers (RV 2017, QRS 2017- industrial track, Qt World Summit 2017) and one poster (Journées du GDR GPL 2017) are being submitted.
- The prototype monitoring tool was released on the project’s forge (https://forge.imag.fr/projects/modmed ) as an open source tool, as well as two releases of the C++ structured trace library.

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.