Main Goals


The MCPS industry does not yet embrace Formal Methods for several reasons:

  • the whole MCPS formalisation and runtime verification seems out of reach because their use is not sufficiently constrained and their sensors offer a very limited sense of their environnement.
  • Formal Methods are perceived as requiring new skills and considerable upfront work, in addition to the work already invested in system design.
  • proposed tools are frequently not adapted: they do not support the most used programming language (C++) or they require a technological revolution (code generation) or they are based on esoteric formalisms (LTL).

Those efforts seem too much regarding the considered risks and their benefits seem too uncertain. An approach requiring the minimum of effort and upfront changes is necessary to gain adoption in the development of rarely critical software such as MCPS.

 

the MODMED project embraces the verification of runtime trace properties to meet this goal and proposes tools that limit developers efforts. Expected benefits for MCPS are numerous :

  1. Critical pre-requisites and requirements will be best understood by the formalisation of trace properties.
  2. System tests will be more efficient when supervised by trace properties expressing the pre-requisites and the oracle of each test.
  3. Post-market surveillance will be more relevant than using user surveys.
  4. Properties will allow classifying real medical interventions traces and quantifying MCPS usage.
  5. Troubleshooting recurring problems will be automated.

 

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

Work Programme

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 this targeted Formal Method by other industrials, MODMED results will be presented to academic and industrial conferences (WP7).


The corresponding deliverables can be found on IMAG forge and Deliverables page.