# Model Checking Clinical Decision Support Systems Using SMT

## TL;DR

This paper introduces a framework that translates clinical knowledge artifacts into SMT models for semantic verification, enhancing the safety and reliability of clinical decision support systems.

## Contribution

It presents the first method for semantic verification of clinical knowledge artifacts using SMT solvers, addressing a gap in formal validation.

## Key findings

- Successfully translated logic fragments of KAs into SMT models
- Verified KAs efficiently using Z3 SMT solver
- Demonstrated effectiveness on publicly available KAs

## Abstract

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.