Verification of Clinical Guidelines by Model Checking

Clinical guidelines systematically assist practitioners with providing appropriate health care for specific clinical circumstances. However, a significant number of guidelines are lacking in quality. In this paper, we use the UML modeling language to capture guidelines and model checking techniques for their verification. We have established a classification of possible properties to be verified in a guideline and we present an automated approach based on a translation from UML to PROMELA, the input language of the SPIN model checker. Our approach is illustrated with a guideline based on a guideline published by the National Guideline Clearing House (NGC).

1. Introduction

Clinical guidelines systematically assist practitioners with providing health care for specific clinical circum-stances. They provide important advantages in medical care including the improvement of clinical practice, support for medical decision-making or reduction of inappropriate variations in everyday clinical practice [1], [2]. Because of the vast amount of clinical guidelines, several organizations have undertaken efforts to publish them (using text formats such as HTML or PDF) in the literature and on the internet to make them more accessible and to enable evidence-based knowledge to be reused (see for example [3], [4]).