Formally modelling the software functionality and interactivity of safety-critical devices allows us to prove properties about their behaviours and be certain that they will respond to user interaction correctly. In domains such as medical environments, where many different devices may be used, it is equally important to ensure that all devices used adhere to a set of safety, and other, principles designed for that environment. In this paper we look at modelling important properties of interactive medical devices including safety considerations mandated by their users. We use ProZ for model checking to ensure that properties stated in temporal logic hold, and also to check invariants. In this way we gain confidence that important properties do hold of the device, and that models of particular devices adhere to the properties described.