Medical Cyber-Physical Systems (CPSs) integrating Patients, Devices, and healthcare personnel (Physicians) form safety-critical PDP triads whose dependability is challenged by system heterogeneity and uncertainty in human and physiological behavior. While existing clinical decision support systems support clinical practice, there remains a need for proactive, reliability-oriented methodologies capable of identifying and mitigating failure scenarios before patient safety is compromised. This paper presents M-GENGAR, a methodology based on a closed-loop Digital Twin (DT) paradigm for dependability assurance of medical CPSs. The approach combines Stochastic Hybrid Automata modeling, data-driven learning of patient dynamics, and Statistical Model Checking with an offline critical scenario detection phase that integrates model-space exploration and diversity analysis to systematically identify and classify scenarios violating expert-defined dependability requirements. M-GENGAR also supports the automated synthesis of mitigation strategies, enabling runtime feedback and control within the DT loop. We evaluate M-GENGAR on a representative use case study involving a pulmonary ventilator. Results show that, in 87.5% of the evaluated scenarios, strategies synthesized through formal game-theoretic analysis stabilize patient vital metrics at least as effectively as human decision-making, while maintaining relevant metrics 20% closer to nominal healthy values on average.

翻译：整合患者、设备与医护人员（医师）的医疗信息物理系统构成了安全攸关的PDP三元组，其可靠性因系统异构性及人类与生理行为的不确定性而面临挑战。现有临床决策支持系统虽能辅助临床实践，但仍缺乏能够在患者安全受损前主动识别并缓解失效场景的、面向可靠性的方法论。本文提出M-GENGAR方法，该方法基于闭环数字孪生范式实现医疗信息物理系统的可靠性保障。该方案融合随机混合自动机建模、患者动态数据驱动学习及统计模型检测技术，通过集成模型空间探索与多样性分析的离线关键场景检测阶段，系统性识别并分类违反专家定义可靠性需求的场景。M-GENGAR同时支持缓解策略的自动生成，实现数字孪生闭环内的运行时反馈与控制。我们在涉及肺部呼吸机的典型用例研究中评估M-GENGAR方法。结果表明：在87.5%的评估场景中，通过形式化博弈论分析生成的策略能使患者生命体征至少达到与人工决策相当的稳定效果，同时使相关指标平均更接近正常健康值20%。