安全医疗设备控制的形式化定义模式的分布式实时仿真

医疗设备及其互操作的安全性是一个尚未解决的问题，以令人震惊的频率导致患者发生严重甚至致命的事故。形式化方法，特别是支持高度可重用且可证明安全的模式（这些模式可以实例化为许多设备实例），可以在这一方面提供帮助。然而，如何从逻辑时间中的形式化规约过渡到能够在物理时间中与其他设备以及患者和/或医生行为的仿真进行互操作的可执行仿真，这仍然是一个悬而未决的问题。本工作提出了一种基于规约的方法，其中虚拟仿真环境可以很容易地从实时 Maude 中的形式化规约开发出来，并能够支持与其他真实设备和仿真模型的交互。这一通用方法被详细解释，并通过两个具体场景进行说明，这两个场景都是一个通用安全形式化模式的实例：一个场景涉及可证明安全的起搏器与仿真心脏的交互；另一个涉及患者自控镇痛的安全控制器与真实注射泵的交互。