This work is the result of a collaboration of the HCI and Formal Methods group at the University of Waikato. A big NZ health care company had given us a specification of a safety-critical medical device. We employed a hybrid modelling technique, which draws from interaction design and formal methods, to analyse the safety of the device and important issues such as the reachability of all menu states. I modelled the user interaction; a research assistant modelled the underlying functionality. In team-work, we combined the two models.