使用 SMT 对临床决策支持系统进行模型检测
软件工程
2019-03-06 v2
摘要
单个临床知识构件（KA）旨在用于现代医疗系统临床决策支持（CDS）系统中的诊疗点，以提供安全、循证的照护。对于 KA 的形式化编写，语法验证与确认由文法保证。然而，目前尚无语义验证方法。任何语义谬误都可能导致照护提供者对结果予以拒收。作为解决该问题的第一步，我们提出了一个将 KA 的逻辑片段翻译为可满足性模理论（SMT）模型的框架。我们通过自动翻译公开可用 KA 的逻辑片段并使用 Z3 SMT 求解器对其进行验证，展示了我们工作的有效性与效率。
引用
@article{arxiv.1901.04545,
title = {Model Checking Clinical Decision Support Systems Using SMT},
author = {Mohammad Hekmatnejad and Andrew M. Simms and Georgios Fainekos},
journal= {arXiv preprint arXiv:1901.04545},
year = {2019}
}
备注
6 pages, 2 listings, 2 tables