模型与整合医疗资源可用时间及关系在可验证的正确可执行医疗最佳实践指南模型中（扩展版）
Model and Integrate Medical Resource Available Times and Relationships in Verifiably Correct Executable Medical Best Practice Guideline Models (Extended Version)
AI总结：
本文提出了一种分离模型和联合验证（SMJV）架构，用于分别建模医疗资源的可用时间和关系，并与现有可执行医疗最佳实践指南模型联合验证安全性属性，以提高医疗资源管理在紧急护理中的安全性和有效性。
摘要：
提高患者护理安全性是医疗网络物理系统的目标。最近的研究表明，通过计算机化医疗最佳实践指南可以显著降低患者死亡率。最近的数据也显示，一些急诊护理中的发病率和死亡率直接由资源不足导致的治疗延迟或中断引起。然而，医疗指南通常不提供关于医疗资源需求以及如何管理潜在的资源可用性延迟的指导。如果医疗资源暂时不可用，现有可执行医疗指南模型的安全属性可能会失效，从而增加患者的风险。本文提出了一种分离模型和联合验证（SMJV）架构，用于分别建模医疗资源的可用时间和关系，并与现有医疗最佳实践指南模型联合验证安全性属性，其中资源模型被整合在内。SMJV架构允许医疗人员在紧急护理中有效管理医疗资源需求和意外资源可用性延迟。分离建模方法还允许不同领域的专业人士独立修改模型，有助于管理频繁的资源可用性变化，并在多个医疗指南模型中重用资源状态图。一个简化中风场景被用作案例研究，以检验SMJV架构的有效性和有效性。案例研究表明，SMJV架构能够识别由意外资源延迟引起的不安全属性。
英文摘要：
Improving patient care safety is an ultimate objective for medical cyber-physical systems. A recent study shows that the patients' death rate is significantly reduced by computerizing medical best practice guidelines. Recent data also show that some morbidity and mortality in emergency care are directly caused by delayed or interrupted treatment due to lack of medical resources. However, medical guidelines usually do not provide guidance on medical resource demands and how to manage potential unexpected delays in resource availability. If medical resources are temporarily unavailable, safety properties in existing executable medical guideline models may fail which may cause increased risk to patients under care. The paper presents a separately model and jointly verify (SMJV) architecture to separately model medical resource available times and relationships and jointly verify safety properties of existing medical best practice guideline models with resource models being integrated in. The SMJV architecture allows medical staff to effectively manage medical resource demands and unexpected resource availability delays during emergency care. The separated modeling approach also allows different domain professionals to make independent model modifications, facilitates the management of frequent resource availability changes, and enables resource statechart reuse in multiple medical guideline models. A simplified stroke scenario is used as a case study to investigate the effectiveness and validity of the SMJV architecture. The case study indicates that the SMJV architecture is able to identify unsafe properties caused by unexpected resource delays.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
