Verification of Medical Guidelines by Model Checking -- A Case Study

The paper presents the process of formal modeling and verification of guidelines using the modeling language Asbru, temporal logic for expressing the quality requirements, and model checking for proof and error detection. The approach is illustrated with a case study on a guideline by the American Association for Pediatrics on "Jaundice in healthy Newborns".