Improving the trustworthiness of medical device software with formal verification methods

Chunxiao Li, Anand Raghunathan, Niraj K. Jha

Research output: Contribution to journalArticlepeer-review

29 Scopus citations


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.

Original languageEnglish (US)
Article number6574212
Pages (from-to)50-53
Number of pages4
JournalIEEE Embedded Systems Letters
Issue number3
StatePublished - 2013

All Science Journal Classification (ASJC) codes

  • Control and Systems Engineering
  • General Computer Science


  • Formal verification
  • Medical device software
  • Safety
  • Security


Dive into the research topics of 'Improving the trustworthiness of medical device software with formal verification methods'. Together they form a unique fingerprint.

Cite this