互操作医疗系统中时序属性的规范与验证
Specification and Verification of Timing Properties in Interoperable Medical Systems
AI总结：
针对互操作医疗系统时序属性验证，提出基于Timed Rebeca的正式规范与模型检验方法，并利用模式静态属性约简状态空间，经临床场景验证有效。
摘要：
为支持在护理点将各种设备/应用动态组合成医疗系统，已提出一组通信模式来描述设备的通信需求。为满足时序要求，每种模式将常见时序属性细化为可由组件本地执行的更细粒度属性。底层通信基础设施的常见时序要求由这些本地属性推导得出。设备的本地属性由供应商在开发时保证。尽管组织采购的设备在本地属性和中间件方面兼容，但它们可能无法按预期运行。组织网络的延迟与设备的本地属性相互作用。为验证组件时序属性与网络之间的交互，我们在Timed Rebeca中正式规范此类系统。我们使用模型检验来验证通信基础设施的推导时序要求，基于网络和设备模型。我们提供一组模板作为指南，以正式模式模型来规范医疗系统。使用多个设备的复合医疗系统面临状态空间爆炸问题。我们基于模式的静态属性扩展了Timed Rebeca的约简技术。我们证明我们的约简是可靠的，并通过建模两个由多个模式实例组成的临床场景，展示了我们的方法在减少状态空间方面的适用性。
英文摘要：
To support the dynamic composition of various devices/apps into a medical system at point-of-care, a set of communication patterns to describe the communication needs of devices has been proposed. To address timing requirements, each pattern breaks common timing properties into finer ones that can be enforced locally by the components. Common timing requirements for the underlying communication substrate are derived from these local properties. The local properties of devices are assured by the vendors at the development time. Although organizations procure devices that are compatible in terms of their local properties and middleware, they may not operate as desired. The latency of the organization network interacts with the local properties of devices. To validate the interaction among the timing properties of components and the network, we formally specify such systems in Timed Rebeca. We use model checking to verify the derived timing requirements of the communication substrate in terms of the network and device models. We provide a set of templates as a guideline to specify medical systems in terms of the formal model of patterns. A composite medical system using several devices is subject to state-space explosion. We extend the reduction technique of Timed Rebeca based on the static properties of patterns. We prove that our reduction is sound and show the applicability of our approach in reducing the state space by modeling two clinical scenarios made of several instances of patterns.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
