The MODMED project is a rare opportunity to spread Formal Methods to new domains, starting with Medical Cyber-Physical Systems (MCPS)!

These MCPS combine data from novel sensors and existing modalities like scanners with elaborate software processing to assist caregivers as flight control systems help a pilot flying planes, making their interventions safer. Their whole formalisation is out of reach but our “targeted” Formal Method allows verifying a reduced number of critical properties on their execution traces in a safer, more factual and efficient way than current industry practices (reviews, manual tests). Especially once MCPS are used in the field!

This method embraces an iterative approach one can describe as “USE and OBSERVE a system to IMPROVE it”, and tackles several challenges :
  • Better trace (without effort) and explore (without getting lost) the traces of a system thanks to a C++ structured traces library
  • FORMALIZE and EVALUATE critical requirements or complex problems with a trace properties language with appropriate abstraction level and trace monitoring and analysis tools

MODMED studied a MCPS guiding Total Knee Arthroplasties (TKA) to design the method and implement adapted tools available on the GRICAD's Gitlab:
  • modmedLog: a C++ structured trace library adapted to industry constraints
  • ParTraP: a Domain-Specific Language (DSL) for critical or complex MCPS requirements as execution Trace Properties and monitor to evaluate the properties on pre-processed execution traces
The MODMED consortium keeps working on:
  • a standard trace format and domain vocabulary
  • adapting the DSL to directly work on execution traces without pre-processing
  • tools for understanding traces, evaluating the quality of tests, generating monitors, etc. 
These open source tools will be used by MCPS manufacturers in relation with the MODMED Consortium which gathers:
  •  a medical device manufacturer: 
    Blue Ortho

  • a research team:
    LIG   VASCO
  • and a software components and services provider for Computer-Assisted Surgery:
    MinMaxMedical

The project is partly funded by ANR-15-CE25-0010