Verification of Careflow Management Systems with Timed BDICTL Logic

Health care workflows (careflows) involve complex, distributive processes with a high degree of variability. There are ubiquitous communication and massive data and knowledge management requirements and the processes are time sensitive, involve complex timing requirements, and are safety critical. Designing these processes and managing their performance is difficult and error prone. Using verification techniques, mathematical methods of proving correctness, we can reduce errors and ensure that the processes satisfy their specifications. We present a prototype next-generation multi-threaded model checker to reason about timed processes in careflows sensitive to patient preferences and the goals of the careteam using a temporal logic extended with modalities of beliefs, desires and intentions.