TY - GEN
T1 - MediK
T2 - 23rd International Conference on Formal Methods in Computer-Aided Design, FMCAD 2023
AU - Saxena, Manasvi
AU - Song, Shuang
AU - Sha, Lui
N1 - Publisher Copyright:
© 2023 FMCAD Association and individual authors.
PY - 2023
Y1 - 2023
N2 - Clinical Best Practice Guidelines (BPGs) are systematically developed, evidence-based statements published by medical institutions and associations that standardize diagnosis and treatment for various clinical scenarios. When expressed in an executable medium, BPGs can be utilized to build systems that assist healthcare professionals (HCPs) with situation-specific advice. Such systems, known as Guideline-based Clinical Decision Support Systems (CDSSs), have been shown to improve patient outcomes.Several Domain-Specific Languages (DSLs) have been proposed to facilitate expressing BPGs in a computer-interpretable format that is easily comprehensible to HCPs. Given the safety-critical nature of CDSSs, the need for such languages to have complete formal semantics and an ecosystem of formal analysis tools has been recognized. Moreover, since these languages evolve over time to accommodate complexities in modeling BPGs, tools for them must also be adaptable to changes. But, existing languages lack complete formal semantics, or analysis tools derived from them.This work introduces MediK: a new DSL for expressing BPGs with a complete executable formal semantics, and formal analysis tools, including a model checker, symbolic execution engine, and deductive verifier. As MediK's tools are derived from its semantics, any update to the language is automatically reflected across all tools. To evaluate our approach, we collaborated with a major pediatric hospital to develop a MediK-based CDSS for the screening and management of Pediatric Sepsis and validated that it satisfies desired safety properties. Our CDSS is Institutional Review Board (IRB) approved and is slated to undergo clinical simulations.
AB - Clinical Best Practice Guidelines (BPGs) are systematically developed, evidence-based statements published by medical institutions and associations that standardize diagnosis and treatment for various clinical scenarios. When expressed in an executable medium, BPGs can be utilized to build systems that assist healthcare professionals (HCPs) with situation-specific advice. Such systems, known as Guideline-based Clinical Decision Support Systems (CDSSs), have been shown to improve patient outcomes.Several Domain-Specific Languages (DSLs) have been proposed to facilitate expressing BPGs in a computer-interpretable format that is easily comprehensible to HCPs. Given the safety-critical nature of CDSSs, the need for such languages to have complete formal semantics and an ecosystem of formal analysis tools has been recognized. Moreover, since these languages evolve over time to accommodate complexities in modeling BPGs, tools for them must also be adaptable to changes. But, existing languages lack complete formal semantics, or analysis tools derived from them.This work introduces MediK: a new DSL for expressing BPGs with a complete executable formal semantics, and formal analysis tools, including a model checker, symbolic execution engine, and deductive verifier. As MediK's tools are derived from its semantics, any update to the language is automatically reflected across all tools. To evaluate our approach, we collaborated with a major pediatric hospital to develop a MediK-based CDSS for the screening and management of Pediatric Sepsis and validated that it satisfies desired safety properties. Our CDSS is Institutional Review Board (IRB) approved and is slated to undergo clinical simulations.
KW - Model checking
KW - Semantics
UR - http://www.scopus.com/inward/record.url?scp=85180373385&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=85180373385&partnerID=8YFLogxK
U2 - 10.34727/2023/isbn.978-3-85448-060-0_39
DO - 10.34727/2023/isbn.978-3-85448-060-0_39
M3 - Conference contribution
AN - SCOPUS:85180373385
T3 - Proceedings of the 23rd Conference on Formal Methods in Computer-Aided Design, FMCAD 2023
SP - 306
EP - 317
BT - Proceedings of the 23rd Conference on Formal Methods in Computer-Aided Design, FMCAD 2023
A2 - Nadel, Alexander
A2 - Rozier, Kristin Yvonne
A2 - Hunt, Warren A.
A2 - Weissenbacher, Georg
PB - Institute of Electrical and Electronics Engineers Inc.
Y2 - 24 October 2023 through 27 October 2023
ER -