Improving the trustworthiness of medical device software with formal verification methods

Wearable and implantable medical devices are commonly used for diagnosing, monitoring, and treating various medical conditions. Increasingly complex software and wireless connectivity have enabled great improvements in the quality of care and convenience for users of such devices. However, an unfortunate side-effect of these trends has been the emergence of security concerns. In this letter, we propose the use of formal verification techniques to verify temporal safety properties and improve the trustworthiness of medical device software. We demonstrate how to bridge the gap between traditional formal verification and the needs of medical device software. We apply the proposed approach to cardiac pacemaker software and demonstrate its ability to detect a range of software vulnerabilities that compromise security and safety.