A User-friendly Tool for Model Checking Healthcare Workflows

Workflow management tools may be used in many domains, to guide and direct processes, to support monitoring activities and to increase organizational efficiency. In safety critical applications such as healthcare, it is essential that the workflow is error-free, that is, for every run of the workflow, necessary requirements are satisfied and unwanted situations do not occur. However, most tools and frameworks which support workflow specification are not formal enough to allow automated verification and/or are not user-friendly enough for the domain experts to use. In this paper we discuss an extension to a model-driven engineering (MDE) based approach to workflow modelling. Our goals are to provide a framework that can model typical healthcare protocols, by means of a visual tool which can be easily understood by the users (usually clinicians), and to articulate and model check behavioural properties. With this tool, the user can input a workflow model and workflow properties which are defined diagrammatically; the model is automatically transformed to DVE code (the DiVinE model checker's language) and the properties to LTL-formulae. If the workflow model is not valid wrt. a property, the tool provides a visual representation of a path which is a counter- example that can be easily analysed for debugging. The inherent agility of the MDE approach is especially useful in a healthcare setting because workflows, even for widely used clinical guidelines, generally need to be customized to local settings and updated frequently due to changing conditions, new medications or new research.