Precision in Practice: A Formal Verification Method of Hand Hygiene Behaviors in Anesthesia Induction

Within the operating room, the anesthesia work environment (AWE) has been a primary contributor to healthcare associated infections (HAIs). This is usually attributed to a lack of hand hygiene compliance in anesthesia professionals. However, due to the fast-paced and complex nature of the AWE, a complete picture of how infectious agents spread throughout the AWE is unknown. This paper describes a novel computational approach using formal verification with model checking that can prove whether the cleanliness of each item within a model of an AWE is maintained and, if not, show how the failure occurred. We applied this method to the analysis of the anesthesia induction process of the Auckland Academic Health Alliance. We use the results of this analysis to recommend hand hygiene interventions that will address discovered problems.