Reasoning about clinical guidelines based on algebraic data types and constraint logic programming

Abstract Previously, the authors presented an overall framework aimed at improving the representation, quality and application of clinical guidelines in daily clinical practice. Regarding the quality improvement of guidelines, we developed a proposal to verify specific requirements in guidelines, using the SPIN model checker as verification tool. Additionally, we established a pattern-based approach for defining commonly occurring types of requirements in guidelines, in order to help non experts in their formal specification. In particular, among such patterns, we identified several which could not be verified by using such a proposal, thus leaving their verification as future work. In this paper, we provide a revised and extended version of that work by providing an overall proposal which mainly addresses previous shortcomings, while providing additional verification functionalities. More specifically, we have defined a complementary proposal to the previous one regarding the verification of guidelines. This proposal uses Formula, a model finding and design space exploration tool that is based on Algebraic Data Types (ADT) and Constraint Logic Programming (CLP). The main contributions of this paper are twofold: (1) providing a more complete set of patterns for defining commonly occurring types of requirements in guidelines, and (2) supporting the verification of a wider range of patterns by combining the use of our previous proposal, based on the SPIN model checker, with our Formula-based method. More specifically, our Formula-based proposal provides us with a solution to the verification of those patterns we were not able to verify previously. Additionally, our proposal has been implemented as an Eclipse plug-in developed based on Model Driven Development (MDD) techniques, which enables us to automatically generate the Formula specification of a guideline, making the process faster and less error-prone than a manual translation. This Formula specification, together with the requirements to be checked in the guideline, are finally taken as input of the Formula tool to check whether the guideline verifies the requirements. We show the feasibility of our overall approach by verifying properties in different clinical guidelines with encouraging results.