A poor design interface can contribute to major problems within a medical computing environment. The biggest problem is user error. This can range from treating the wrong patient to entering the wrong value into a medical device.

The authors use a common medical device (an infusion pump) as an example. They selected this device as a target for a formal verification framework for the integration of predicting bounds for task-completion times and detecting user-error-related design flaws. The authors formalize a generic user model (GUM) and code it for use within the Symbolic Analysis Laboratory (SAL, http://sal.csl.sri.com) language. Using the infusion pump model, within the SAL language environment, they propose changes to the operation of the infusion pump in order to predict and possibly avoid erroneous behaviors.

This is an important paper that will attract attention from people within a medical computing environment who may not be familiar with the methods associated with formal aspects of computing. Basing their infusion pump model on code written for the SAL language may frustrate people outside the formal aspects of computing environment. The authors hint that future papers will be written using the infusion pump model. If they continue to base these papers on the SAL language, they should provide some mechanism to download the source code and also give some examples within an appendix on how to run the source code using the SAL language. Despite these criticisms, this was a fascinating paper to read. It will be interesting to follow the authors’ future work.