基于SMT的临床决策支持系统模型检验
Model Checking Clinical Decision Support Systems Using SMT
摘要：
个体临床知识工件（KA）设计用于护理点的临床决策支持（CDS）系统，以在现代医疗保健系统中提供安全的循证护理。对于KA的正式创作，语法验证和确认由语法保证。然而，还没有语义验证的方法。任何语义谬误都可能导致护理提供者拒绝结果。作为解决这个问题的第一步，我们提出了一个框架，用于将KA的逻辑段转换为可满足性模理论（SMT）模型。我们提出了我们的工作的有效性和效率，通过自动翻译公开可用的KA的逻辑片段，并使用Z3 SMT求解器验证它们。
英文摘要：
Individual clinical Knowledge Artifacts (KA) are designed to be used in Clinical Decision Support (CDS) systems at the point of care for delivery of safe, evidence-based care in modern healthcare systems. For formal authoring of a KA, syntax verification and validation is guaranteed by the grammar. However, there are no methods for semantic verification. Any semantic fallacy may lead to rejection of the outcomes by care providers. As a first step toward solving this problem, we present a framework for translating the logical segments of KAs into Satisfiability Modulo Theory (SMT) models. We present the effectiveness and efficiency of our work by automatically translating the logic fragment of publicly available KAs and verifying them using Z3 SMT solver.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
