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

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.

An Overview of Medical Device Software
Medical devices address a continuum of diagnosis and treatment applications varying in complexity from digital thermometers, insulin pumps, pacemakers, and cardiac monitors to anesthesia machines, large ultrasound imaging systems, chemistry analyzers, and proton beam therapy systems.

As science and technology advance, so does the complexity and capability of next-generation devices. The easily identifiable signature of these devices is that they are intended to directly or indirectly affect public health.

Software is becoming ubiquitous in medical devices and contributing to their complexity. As a result, various worldwide regulatory organizations include language in their directives to explicitly address device software. Recent studies are pointing to increasing failure rates of medical devices due to software coding errors.

The FDA increased its involvement in reviewing the development of medical device software in the mid-1980s, when software coding errors in a radiation therapy device contributed to the lethal overdose of a number of patients. The FDA has published several guidance documents and recognized several standards addressing good software development processes.

More recently, the FDA has established a software laboratory within the Center for Devices and Radiological Health (CDRH) Office of Science and Engineering Laboratories (OSEL) to identify software coding errors in devices under recall investigation. As part of its investigation, the software laboratory examines the source code to understand and identify the root cause of a device failure.

Causes of Device Failures
Code defects that result in run-time errors are the major cause of the embedded device failures mentioned above. Run-time errors are a specific class of software errors called latent faults.

The faults may exist in code, but unless very specific tests are run under particular conditions, the faults may not be realized in the system. In these cases, the code can appear to function normally but when a fault is realized may result in unexpected system failures, sometimes with fatal consequences. Run-time errors may be caused by conditions such as:

- Uninitialized data variables
- Out-of-bounds array access
- Null pointer dereference
- Incorrect computation (for example, divide by zero)
- Concurrent access to shared data
- Illegal type conversion
- Memory leaks
- Unintentional non-terminating loops