Model-Driven Design of Clinical Guidance Systems
  Clinical guidance systems have been widely adopted to help medical staffs to avoid preventable medical errors such as delay in diagnosis, treatment or untended deviations from best practice guidelines. However, because patient condition changes rapidly and medical staffs are usually overloaded in acute care setting, how to ensure the correctness of the system reaction to those rapid changes and managing interaction with physicians remains challenging. In this paper, we propose a domain-specific model-driven design approach to address these challenges for designing clinical guidance systems. Firstly, we translate the relevant medical knowledge described in generic literature and different best practice guidelines into a set of executable and indirectly verifiable finite state machine models. We introduce an organ-centric paradigm to construct clinical models, and also develop a physician model to track physician-system interactions and deviations. Secondly, for verification of the compositional system model, we translate the model into timed automata, based on which, we formalize a set of clinical and system safety requirements as computation tree logic(CTL) formulas and use the UPPAAL model checking tool to formally verify those requirements. In this way, the correctness of the model can be mathematically proved. Finally, we can automatically generate the executable code from the verified model using the corresponding code generation tools for finite state machine. For evaluation, we apply the approach to the design of clinical guidance systems for cardiac arrest. The generated code can be deployed and interact with existing guidance systems. 
Maryam Rahmaniheris, Yu Jiang, Lui Sha
cs.CY