Improving Trace Generation and Analysis for Medical Devices

A new generation of medical devices emerges to supportincreasingly more complex medical decisions and procedures.These Medical Devices (MD) combine data fromnovel sensors and existing modalities like scanners withelaborate software processing to assist caregivers in the sameway Flight Management Systems help a pilot flying planes.For instance, Blue Ortho’s MD allows performing TotalKnee Arthroplasty (TKA, i.e. the placement of a femoraland tibial knee prosthesis) more precisely, potentially dividingthe number of revisions by two [1]. Unfortunately,innovation and safety of such MD is hindered by the currentsoftware verification practices of the MD industry. Someformal methods have demonstrated their effectiveness fordecades in the most safety-critical industries (defense, air,space, railways, nuclear power plants), but they failed togain broader adoption.