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.
E-mail This Article | Printer-Friendly Page |
|
Related Articles
- IC design: A short primer on the formal methods-based verification
- Design-Stage Analysis, Verification, and Optimization for Every Designer
- Verifying embedded software functionality: Combining formal verification with testing
- Using verification coverage with formal analysis
- A Simple New Approach to Hardware Software Co-Verification
New Articles
Most Popular
- System Verilog Assertions Simplified
- System Verilog Macro: A Powerful Feature for Design Verification Projects
- I2C Interface Timing Specifications and Constraints
- Enhancing VLSI Design Efficiency: Tackling Congestion and Shorts with Practical Approaches and PnR Tool (ICC2)
- Dynamic Memory Allocation and Fragmentation in C and C++