Formal methods-based verification of medical device software analysis

摘要

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; infusion pumps may have more than 170,000. Such devices must provide the utmost in safety and reliability.rnMedical device software has typicallyrnbeen verified using code reviews, static analysis and dynamic testing. Code reviews rely solely on the expertise of the reviewer, however, and may not be efficient for large code bases. Traditional static analysis techniques, meanwhile, rely mainly on a pattern-matching approach to detect unsaferncode patterns but cannot prove the absence of run-time errors. And with the increasing complexity of device software, dynamically testing for all types of operating conditions is virtually impossible.