Adopting model checking techniques for clinical guidelines verification.
OBJECTIVE
Clinical guidelines (GLs) are assuming a major role in the medical area, in order to grant the quality of the medical assistance and to optimize medical treatments within healthcare organizations. The verification of properties of the GL (e.g., the verification of GL correctness with respect to several criteria) is a demanding task, which may be enhanced through the adoption of advanced Artificial Intelligence techniques. In this paper, we propose a general and flexible approach to address such a task.


METHODS
Our approach to GL verification is based on the integration of a computerized GL management system with a model-checker. We propose a general methodology, and we instantiate it by loosely coupling GLARE, our system for acquiring, representing and executing GLs, with the model-checker SPIN.


RESULTS
We have carried out an in-depth analysis of the types of properties that can be effectively verified using our approach, and we have completed an overview of the usefulness of the verification task at the different stages of the GL life-cycle. In particular, experimentation on a GL for ischemic stroke has shown that the automatic verification of properties in the model checking approach is able to discover inconsistencies in the GL that cannot be detected in advance by hand.


CONCLUSIONS
Our approach thus represents a further step in the direction of general and flexible automated GL verification, which also meets usability requirements.
Dipartimento di Informatica, Università del Piemonte Orientale "Amedeo Avogadro", Alessandria, Italy.
Alessio
A
Bottrighi
Laura
L
Giordano
Gianpaolo
G
Molino
Stefania
S
Montani
Paolo
P
Terenziani
Mauro
M
Torchio
D000465:Algorithms; D003198:Computer Simulation; D006801:Humans; D017410:Practice Guidelines as Topic / Q000592:standards*; D012985:Software Design