Model Checking Clinical Decision Support Systems Using SMT
This addresses the problem of potential semantic fallacies in clinical decision support systems for healthcare providers, which could lead to rejection of outcomes, though it is an incremental step as it focuses on a first framework for verification.
The authors tackled the lack of semantic verification methods for clinical Knowledge Artifacts (KAs) in Clinical Decision Support (CDS) systems by developing a framework that translates logical segments of KAs into SMT models and verifies them using the Z3 solver, demonstrating effectiveness and efficiency through automatic translation and verification of publicly available KAs.
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.