Verify these devices in conjunction with their working environment

The Medical Cyber-Physical Systems (MCPS) industry did not yet embrace formal methods for several reasons:

• the whole MCPS formalisation seems out of reach because their use is not sufficiently constrained and their sensors offer a limited sense of their environment.
• formal methods require considerable upfront work, in addition to the work already invested in system design.
• proposed tools are frequently not adapted to this industry.

Those efforts seem oversized and their benefits too uncertain in the development of MCPS which are rarely critical software.

MODMED sponsors the verification of runtime trace properties to overcome these challenges and proposes tools that limit developers’ efforts. Expected benefits for MCPS are numerous:

1. Critical pre-requisites and requirements are best understood by the formalisation of trace properties
2. System tests are more efficient when supervised by automated pre-requisites and verdict
3. Post-market surveillance will be more relevant
4. MCPS usage by surgeon is classified and quantified
5. Troubleshooting recurring problems will be automated

The adoption of these formal tools by MCPS industry may initiate broader changes in similar industries.

A “targeted” approach to the formalization of MCPS based on the monitoring of trace properties

MCPS can easily be instrumented to provide execution traces in the field. The mandatory risk analysis identifies critical MCPS requirements. The main challenge remains adoption of formal methods by the industry. Hence, MODMED allows to easily verify a relevant subset of critical requirements, in a precise and reliable way, by monitoring formal execution traces properties.

The project is based on two central contributions: a C++ structured trace library to instrument MCPS with minimal cost (WP2), and a Domain Specific Language (DSL) to express SCPM properties in a way that is intuitive and understandable to engineers (WP1). The project provides tools for the DSL: monitor generator (WP3); test assessment (WP4); traces extraction for other tools (WP5).

Traces and specifications of a real MCPS used in thousands of surgeries have been studied to identify requirements for the DSL (WP6/D1). Project tools were submitted to industrials for the development of new MCPS (WP6/D2). The results of the project have been presented to academic and industrial conferences (WP7) to encourage the adoption of these lightweight formal methods by other industrials.

Main results

The modmedLog C++ library allows producing analyzable traces with no source code change, and then improving them while refactoring the source code.

The ParTraP language allows writing in a readable way many properties with temporal constraints, events data and Python functions. A comprehensive development environment (with syntactic editor, interpreter, compiler to Java) simplifies writing properties and understanding their results.

These tools are available in open source (https://gricad-gitlab.univ-grenoble-alpes.fr/modmed) and received promising feedback from a panel of MCPS developers.

Scientific production and patents

"Requirements for a trace property language for medical devices" presented our lightweight formal approach to the Software Engineering in Healthcare Systems conference in Sweden. ⟨10.1145/3194696.3194699⟩. ⟨hal-02004396⟩

"Enhancing qDebug()" proposal given to Qt Contributors Summit in Berlin lead us to modify modmedLog to attain comparable performance to system tracing libraries.(slides)

"Extending Specification Patterns for Verification of Parametric Traces" presents our academic results in the Proceedings of the 6th Intl Conference on Formal Methods in Software Engineering. ⟨10.1145/3193992.3193998⟩. ⟨hal-02004378⟩

"An Environment for the ParTraP Trace Property Language" describes the ParTraP tools and took the form of a tool demo at the RV 2018 conference, which gathers the scientific community dedicated to runtime verification. ⟨10.1007/978-3-030-03769-7_26⟩. ⟨hal-02004420⟩

Illustration

In an iterative approach to “Use and Observe a system to Improve it”, MODMED allows to 1) Better trace, without effort, and 2) Formalize and Evaluate critical requirements to quantify problems.

Facts

MODMED is a public-private applied research project coordinated by Arnaud Clère from MinMaxMedical which gathered the Laboratoire d’Informatique de Grenoble (VASCO team) and Blue Ortho, a medical devices manufacturer. The project started in October 2015 and lasted 42 months. It received an ANR grant of 550 k€ for an approximate global cost of 1,200 k€.