Model Checking Workflow Monitors and Its Application to a Pain Management Process

Safety critical systems often consist of many complex processes. Monitoring the behaviour of such processes is critical for enforcing policies, and achieving efficiency and reliability goals. The paper presents a new graphical language for modeling monitors for time constrained workflow processes. To ensure the correctness of a monitor system, we present a model checking approach for verification. We provide an automated data aware translation from a monitor model and its associated workflow to DVE, the input language of the DiVinE model checker, reducing the time and effort required for model checking. We prove the correctness of the translation and give a detailed case study involving LTL properties for a compensable healthcare workflow with time constraints and monitors.