A Formal Methods-based verification approach to medical device software analysis

By Paul Jones, Raoul Jetley, and Jay Abraham from The MathWorks
Embedded.com (02/09/10, 11:19:00 AM EST)

Embedded software in medical devices is increasing in content and complexity. State-of-the-art pacemakers may contain up to 80,000 lines of code, while infusion pumps may have more than 170,000 lines of code. These devices must provide the utmost in safety and reliability.

Historically, medical device software has typically been verified using code reviews, static analysis, and dynamic testing. Code reviews rely solely on the expertise of the reviewer and may not be efficient for large code bases.

Traditional static analysis techniques rely mainly on a pattern-matching approach to detect unsafe code patterns, but cannot prove the absence of run-time errors. Lastly, with the increasing complexity of device software, dynamically testing for all types of operating conditions is virtually impossible.

This article explores the application of formal methods"based abstract interpretation techniques to mathematically prove the absence of a defined set of run-time errors. The verification solution is then compared with other software analysis and testing methods, such as code review, static analysis, and dynamic testing.

To read the full article, click here