用于心律失常检测算法的量化正则表达式

出于验证心律失常检测算法正确性的动机，我们用量化正则表达式的语言对这些算法进行了形式化。QRE是一种灵活的形式化语言，用于指定数据流上的复杂数值查询，并提供可证明的运行时间和内存消耗保证。感兴趣的医疗设备算法包括峰值检测（其中心脏信号中的峰值表示一次心跳）以及各种鉴别器，每个鉴别器利用心脏信号的某个特征来区分致命与非致命心律失常。用当前的时序逻辑表达这些算法的期望输出，并通过监控器综合来实现它们，是繁琐的、容易出错的、计算昂贵的，有时甚至是不可行的。相比之下，我们表明，当今心律失常检测设备核心的各种峰值检测器（在时域和小波域中）和各种鉴别器都可以用QRE轻松表达。使用单一形式化方法来描述心律失常检测器期望的端到端操作，为这些检测器的正确性和性能的形式化分析与严格测试开辟了道路。这种分析可以减轻设备开发者在修改其算法时所面临的监管负担。通过在真实患者数据上运行峰值检测QRE，展示了其性能，其结果与心脏病专家提供的结果相当。