A Formal Approach for Detecting Masking in Medical Alarms

The perceptibility of auditory medical alarms is critical to patient health and safety. The delay in responding to auditory medical alarms would have a negative impact on patient health and could lead to dangerous consequences. A relatively understudied source of response failures has to do with masking, a condition where concurrent sounds interact in ways that make one or more of them imperceptible due to physical limitations of human perception. In this work we present a method, that uses a novel combination of psychophysical modeling and formal veri cation with model checking to detect mask- ing in a modeled con guration of medical alarms. We describe how the method was developed over two steps. This dissertation presents these steps and demonstrates the scalability and detection improvements via di erent case studies. Results and future research are discussed.