Analysis of Experiences with the Engineering of a Medical Device Using State-Based Formal Methods

The use of software has become ubiquitous and prevalent in modern medical devices such as hemodialysis machines. Consequently, the failure rate of medical devices due to software faults is also increasing. While next-generation software-intensive medical devices contribute to providing better health care and ease of use, their development is becoming unprecedentedly complex and challenging. The critical nature of this domain - particularly its direct implications on health and safety - requires extraordinary measures to ensure the correct and reliable function of such systems. Formal methods are proven to provide approaches, techniques, and tools for correct engineering of software and systems. However, their use in the contemporary medical software engineering is still marginal. In order to promote the use of (state-based) formal methods and showcase their effectiveness in design and development of critical medical devices, we present the hemodialysis case study challenge problem in this article. We also analyze the novelties and limitations of several solutions implementing the case study and explore research challenges that still need to be addressed in future.