A semantics-first approach to safe guidelines-based clinical decision support

Preventable medical errors (PMEs), characterized by misdiagnosis or mistreatment, pose a significant challenge in healthcare. In the United States, PMEs were estimated to have caused between 44,000 and 98,000 deaths in 1997, rising to more than 250,000 in 2013. Additionally, the financial burden of PMEs to the U.S. economy in 2008 was estimated at $19.5 billion. One strategy to reduce PMEs in medicine is through the use of clinical best practice guidelines (BPGs). BPGs are systematically developed, evidence-based statements published by medical institutions and associations that standardize diagnosis and treatment for various clinical scenarios. BPG-conformance has been linked with reduced rates of PMEs, but, following BPGs in practice can be challenging. Computerized Decision Support Systems (CDSSs) aim to improve conformance by encoding medical knowledge in BPGs and providing HCPs with situation-specific, guideline-conformant advice. Growing evidence suggests that effective CDSSs can reduce PMEs by boosting adherence to best practice guidelines. This work presents a semantics-first approach to implementing safe clinical decision support systems. By semantics-first, we mean that i semantics of medical knowledge is accurately captured in the CDSS, and, ii the semantics of the programming language used to encode medical knowledge is formally defined. At the core of our approach is MediK: a novel domain specific language for expressing best practice guidelines that emphasizes comprehensibility to HCPs, enabling them to validate the accuracy of medical knowledge in its programs. MediK has a complete, executable formal semantics in the K Framework, from which all execution and analysis tools are derived in a correct-by-construction manner. To evaluate our approach, we collaborated with a major pediatric hospital to develop a complex real-world CDSS for the screening and management of Sepsis in pediatric cases, and validated that it satisfies desired safety properties. We outline how our approach improves upon the existing state-of-art, optimizations to address domain-specific needs of healthcare practitioners, and discuss challenges for future work.

Name thesis:degree_name

Ph.D.

Level thesis:degree_level

Dissertation

Discipline thesis:degree_discipline

Computer Science

Grantor

University of Illinois at Urbana-Champaign

Year dc:date

2024

Author dc:creator

• Saxena, Manasvi

Contributors dc:contributor

• Rosu, Grigore
• Meseguer, Jose
• Sha, Lui
• Tasiran, Serdar

• Formal Semantics
• Domain Specific Langauges
• Healthcare Systems
• Model Checking

Statement dc:rights

• Copyright 2024 Manasvi Saxena

Language dc:language

en, eng

Handle dc:identifier

https://hdl.handle.net/2142/127206

OAI record oai:identifier

https://www.ideals.illinois.edu/oai-pmh?verb=GetRecord&metadataPrefix=etdms&identifier=oai%3Awww.ideals.illinois.edu%3A2142%2F127206