支持以状态图开发可验证安全医疗指南的形式化方法

提高患者护理的有效性和安全性是医疗信息物理系统的最终目标。现有许多医疗最佳实践指南，但手册中的大多数现有指南难以被医务人员记忆和临床应用。此外，尽管这些指南已通过临床验证，但仅由医疗专业人员进行的验证并不能为医疗信息物理系统的安全性提供保证。因此，还需要形式化验证。本文为我们开发的用于支持可验证安全医疗指南开发的一个框架给出形式化语义。该框架允许计算机科学家与医疗专业人员合作，将医疗最佳实践指南转化为可执行的 statechart 模型，特别是 Yakindu，从而可以快速原型化并验证医疗功能与性质。现有形式化验证技术，特别是 UPPAAL 时间自动机，被集成到该框架中，以提供验证安全性质的形式化验证能力。然而，框架中使用或内置的某些组件，例如开源 Yakindu 状态图以及从状态图到时间自动机的转换规则，并不具有内置语义。除非为该框架定义形式化语义，否则歧义不可避免，这正是本文所要呈现的内容。