Towards a Probabilistic Model Checking-based Approach for Medical Device Risk Assessment

Medical Devices (MDs) are subject to a Risk Management process to guarantee their safety with respect to risks patients and healthcare operators may experience. Well known classical Probabilistic Risk Assessment (PRA) techniques widely used in the MD sector, such as Failure Model and Effective Critical Analysis (FMEA) and Fault-Tree/Event-Tree do not allow to model the dynamics of hazardous situations which involves interactions among system components, human actions, process operations and the environment. This lack is overcome by using a dynamic PRA (DPRA) approach which aids in specifying risk scenarios. DPRA is extensively used in the nuclear, avionics, and space industries to identify possible accident scenarios, but to the best of our knowledge it is not so in the MD field. In this paper we propose a DPRA approach for MD Risk Assessment which relies on the use of a Probabilistic Model Checking (PMC) technique to perform quantitative analysis of risk scenarios. Particularly, our approach combines the ease of Event Sequence Diagram (ESD) to capture the dynamics of risk scenarios and the Markov Decision Processes formalism used as a stochastic model by which to encode ESD. By using a PMC technique to evaluate the MDP-based risk scenarios, we achieve two main benefits. Firstly, hundreds of different scenario realisations can be analysed in seconds due to the computational effectiveness of current PMC algorithms. Secondly, since such technique is based on a state-transition representation, we take advantage of the reachability analysis of states within the risk scenario state space to also quantify the effectiveness of control mechanisms or mitigation actions used to prevent and/or reduce the MD exposition to risk factors. Our ultimate objective is to derive an intuitive, easy, and computationally efficient formal method to perform quantitative risk scenario analysis oriented towards increasing the MD safety. We have applied our approach to an actual MD taken as a case study to demonstrate the features of our DPRA solution.