A Verified, Executable Formalism for Resilient and Pervasive Guideline-Based Decision Support for Patients.

We present an executable formalism for clinical practice guidelines, with the aim of providing pervasive and evidence-based decision support to patients. Unlike traditional formalisms that capture the control flow between tasks, we focus on data flow, with tasks modeled as processes that execute in parallel. By parallelizing and distributing guideline knowledge, each device that constitutes the patient's pervasive healthcare system can provide decision support independently, avoiding single points of failure. This distribution also enables dynamic system re-configurations, increasing its resilience against evolving requirements and changing communications environments. Our model recognizes four types of processes: Monitoring, Analysis, Decision and Effectuation. These processes were specified using (axiomatic) set theory and implemented as a set of libraries on top of Rosette, which supports execution of the formalism and verification of it using constraint solvers. The formalism was also tested by formalizing a complete clinical guideline for diabetes management, which yielded a Rosette program that was then tested on simulated patient data. The major point of clinical relevance is enhancing the quality and safety of decision support delivered to patients.