研究目的

Because of its ability to detect problems in complex concurrent systems, formal verification should be capable of detecting if masking can manifest in a particular configuration of medical alarms. The work presented here demonstrates that this is possible. We developed a method that allows an analyst to specify a configuration of alarms and use formal verification to detect if there are any situations where each alarm is masked.

研究成果

This study has introduced a novel method for identifying masking in configurations of medical alarms. This method uses a formal modeling architecture, psychoacoustic models of masking, specification property patterns, and formal verification with model checking to prove whether or not each alarm in a modeled configuration will be perceptible with normal hearing. The method has the potential to significantly improve patient safety by allowing healthcare providers to evaluate the safety of different medical alarm configurations before they are deployed.

研究不足

The current implementation of the method uses the spreading function from the MPEG2 audio codec for normal hearing, which may not account for individuals with different hearing proficiencies. Additionally, the method does not account for additive masking or temporal masking, and it is uncommon for alarms to be operating in a completely quiet environment.