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

Area of Science:

• Medical Informatics
• Software Engineering
• Formal Methods

Background:

• Clinical guidelines require robust verification for quality and daily practice integration.
• Previous work introduced a framework and SPIN model checker for guideline verification.
• Limitations existed in verifying certain requirement patterns.

Purpose of the Study:

• To address shortcomings in previous guideline verification methods.
• To extend the range of verifiable requirement patterns in clinical guidelines.
• To improve the formal specification and verification process for clinical guidelines.

Main Methods:

• Developed a complementary proposal using the Formula tool (ADT and CLP-based).
• Combined the existing SPIN model checker approach with the new Formula-based method.
• Implemented the proposal as an Eclipse plug-in using Model Driven Development (MDD) techniques for automated specification generation.

Main Results:

• Successfully verified previously unverifiable requirement patterns using the Formula tool.
• Demonstrated a more complete set of patterns for defining guideline requirements.
• Showcased the feasibility of the integrated approach through verification of properties in diverse clinical guidelines.

Conclusions:

• The combined SPIN and Formula-based approach significantly enhances clinical guideline verification capabilities.
• Automated generation of guideline specifications via MDD reduces errors and speeds up the process.
• The improved verification framework supports better quality and application of clinical guidelines in practice.