Modeling and Verifying Timed Compensable Workflows and an Application to Health Care

Over the years, researchers have investigated how to provide better support for hospital administration, therapy and laboratory workflows. Among these efforts, as with any other safety critical system, reliability of the workflows is a key issue. In this paper, we provide a method to enhance the reliability of real world workflows by incorporating timed compensable tasks into the workflows, and by using formal verification methods (e.g., model checking). We extend our previous work [1] with the notion of time by providing the formal semantics of Timed Compensable WorkFlow nets (CWFT-nets). We extend the graphical modeling language of Nova WorkFlow (a workflow management system currently under development) to model CWFT-nets and enhance Nova WorkFlow’s automatic translator to translate a CWFT-net into DVE, the modeling language of the distributed LTL model checker DiVinE. These enhancements provide a method for rapid (re)design and verification of timed compensable workflows. We present a real world case study for Seniors’ Care, developed through collaboration with the local health authority.