设计可验证正确的模型模式以利用状态图建模医疗最佳实践指南（技术报告）

提升患者护理安全性是医疗信息物理系统的终极目标。近期一项研究表明，将医疗最佳实践指南计算机化可显著降低患者死亡率。为便利计算机化医疗最佳实践指南的开发，状态图常作为建模工具使用，因其与疾病和治疗模型高度相似，且能够提供快速原型开发与临床验证仿真。然而，某些状态图实现（如 Yakindu 状态图）基于优先级并具有同步执行语义，导致难以建模医疗指南建模中必不可少的功能，如双向通信与可配置执行顺序。我们未引入新状态图元素或改变状态图实现的底层语义，而是利用现有基本状态图元素为常见问题描述模型模式。具体而言，我们展示了双向通信与可配置执行顺序的模型模式设计，并形式化证明了这些模型模式的正确性。我们进一步以简化的气道激光手术场景为案例，演示所开发模型模式如何解决双向通信与可配置执行顺序问题，及其对医疗安全属性验证与确认的影响。