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

A Formal Methods-based verification approach to 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, 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.

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

Software Verification and Testing
Traditional software verification and testing consists of code reviews and dynamic testing. This section discusses these methods and introduces the application of formal methods”based abstract interpretation to code verification.

Code Review. The code review approach involves describing the team that will perform the review (moderator, designer, coder, and tester), preparing for the review (which involves creating a checklist), and performing the inspection itself. The stated objective is to find errors in code.

Processes on conclusion of the review are also described. These processes include rework to address errors found and follow-up to ensure that issues and concerns raised during inspection are resolved. Another aspect of code review can involve checking compliance to certain coding standards such as MISRA C or JSF++ (for C and C++).

Dynamic Testing. Dynamic testing verifies the execution flow of software, including decision paths, inputs, and outputs. Dynamic testing involves creating test cases, test vectors and oracles, and executing the software against these tests. The results are then compared with expected or known correct behavior of the software.

Because the number of execution paths and conditions increases exponentially with the number of lines of code, testing for all possible execution traces and conditions for the software is impossible.

Static Analysis. Code inspections and testing can reduce coding errors; however, experience has shown that the process needs to be complemented with other methods. One such method is static analysis. This somewhat new method largely automates the software verification process.

The technique attempts to identify errors in the code, but does not necessarily prove their absence. Static analysis is used to identify potential and actual defects in source code.

The static analysis process utilizes heuristics and statistics and does not require code execution or test case development. The process can be thought of as performing strong compiler-type checks (e.g., checking if variables are always initialized or used) to more sophisticated dataflow-based analysis.

These tools may find some errors in code, but there can be a high false positive rate. A false positive occurs when reliable code is identified as an error. The time and energy spent on tracking a false positive can be frustrating for software engineers.

In addition to false positives, it is also important to understand false negatives. A false negative occurs when the static analysis tool fails to identify an error. Unfortunately, decreasing the probability of false negatives increases the probability of false positives.

The use of static analysis can provide a certain amount of automation in the verification process, but this advantage must be weighed carefully against the capability of such tools to generate false positives and false negatives.

Formal Methods-based Verification
The term formal methods is typically applied to proof-based verification of a system with respect to its specification. The term can also be applied to a rigorous mathematical approach of proving code correctness.

This approach may help reduce false negatives—that is, the inability to conclusively state that the code is free of certain types of run-time errors. The next section describes the use of abstraction interpretation as a formal methods”based verification solution that can be applied to software programs.

Abstract Interpretation Abstract interpretation is best explained through a simple example. Consider the multiplication of three large integers:

-4586 – 34,985 – 2389 = ?

For the mathematical problem defined, it is difficult to quickly compute the final value by hand. However, if we abstract the result of the computation to the sign domain (that is, either positive or negative), it is easy to understand that the sign of the computation will be negative.

Determining the sign for this mathematical computation is an application of abstract interpretation. The technique enables us to know precisely some properties of the final result (in this example, the sign ) without having to multiply the integers fully.

We also know that the sign will never be positive for this computation. In fact, abstract interpretation can prove that the sign of the operation will always be negative and never positive.

The concept of soundness is important in the context of a discussion on abstract interpretation. Soundness implies that when assertions are made about a property, those assertions can be proven to be correct.

The results from abstract interpretation are considered sound because it can be mathematically proven with structural induction that the abstraction will predict the correct outcome.

When applied to software programs, abstract interpretation can be used to prove certain properties of software, for example, to prove that the software will not exhibit certain run-time errors.

To see the application of abstract interpretation to code verification, consider the following operation in code:

X = X / (X – Y)

Several issues could cause a potential run-time error. These run-time errors include:

1. Variables that are not initialized
2. An overflow or underflow on the subtraction operation
3. An overflow or underflow on the division operation
4. Divide by zero (if X is equal to Y)
5. Overflow or underflow, depending on the assignment to X

Let us examine condition 4, divide by zero. Plotting X and Y as shown in Figure 1 below , one can see that the 45? line representing X = Y would result in a run-time error. The scatter plot shows all possible values for X and Y when the program executes this line of code.

Figure 1: Plot of data for X and Y.

Dynamic testing would utilize enumeration over various combinations of X and Y to determine if there will be a failure. However, given the large number of tests that would have to be run, this type of testing may not detect or prove the absence of the divide-by-zero run-time error.

Another methodology would be to apply “type analysis” to examine the range of X and Y in the context of the run-time error condition (that is, X = Y). In Figure 2 below , note the bounding box created by type analysis.

If the bounding box intersects X = Y, there is a potential for failure. Some static analysis tools apply this technique. However, type analysis in this case is too pessimistic, since it includes unrealistic values for X and Y.

Figure 2: Type analysis.

With abstract interpretation, a more accurate representation of the data ranges of X and Y is created. Because various programming constructs (such as pointer arithmetic, loops, if-then-else, multitasking) could influence the values of X and Y, an abstract data set is defined.

A simplified representation of this concept is to consider the grouping of the data as polyhedron, as shown in Figure 3 below . If a polyhedron does not intersect X = Y, we can conclusively say that a division by zero will not occur.

Figure 3: Abstract interpretation.

As described earlier, abstract interpretation is a sound verification technique. With abstract interpretation, assertions regarding the specified run-time aspects of the software are proven to be correct.

A Code Verifier Based on Abstract Interpretation
The abstract interpretation concept can be generalized as a toolset that can be used to detect a wide range of run-time errors in software. In this article, we use PolySpace as an example to explain how such a tool can help detect and prove the absence of run-time errors such as overflows, divide by zero, and out-of-bound array access.

Figure 4: Explanation of colors used in PolySpace code verification products

PolySpace code verification software from The MathWorks utilizes abstract interpretation. The input to the software is C, C++, or Ada source code. The output is source code displayed in four colors. As described in Table 1 above and as shown in Figure 5 below , PolySpace results inform the user of the quality of the code using this color-coded scheme.

Figure 5: Sample code verified using PolySpace verification products.

The application of abstract interpretation using PolySpace code verifiers is explained with the following example below . Consider the function:

1 int where_are_errors(int input)
2 {
3 int x, y, k;
5 k = input / 100;
6 x = 2;
7 y = k + 5;
8 while (x < 10)="" 9="">
10 x++;
11 y = y + 3;
12 }
14 if ((3*k + 100) > 43)
15 {
16 y++;
17 x = x / (x - y);
18 }
20 return x;
21 }

The goal in the example above is to identify run-time errors in the function where_are_errors() . The function performs various mathematical computations and includes a while loop and an if statement.

Note that all variables are initialized and used. On line 17, a potential divide by zero could occur if x = y. The question then is that given the control structures and mathematical operations on x and y, could x = y ?

As shown in Figure 6 below , the PolySpace code verifier proves there are no run-time errors in this code. This is because line 17 is executed only when the condition (3*k + 100 > 43) evaluates to true.

Moreover, since the value of y is dependent on that of k, the PolySpace code verifier determines that at line 17, while x is equal to 10, y will always have a value greater than 10. As a result, there cannot be a divide-by-zero error at this line.

This result is determined efficiently without the need to execute code, write test cases, add instrumentation in source code, or debug the code. The verifier also identifies all aspects of code that could potentially have a run-time error. These aspects are underlined (Figure 6 below ).

Figure 6: PolySpace code verification results for safe code.

Because there are no run-time errors in this example, the underlined code is displayed in green. For example, on line 17, the underlined green on the division operator (/) indicates that this operation cannot overflow or have a division by zero.

Code Verification and Medical Device Software
The use of abstract interpretation”based code verification to ensure high quality and reliability of critical software is not new. It is used in many industry sector applications such as avionics, vehicle control systems, and communication systems. Applying this verification methodology to medical device software has several advantages.

Using tools based on this technique, software development and quality teams are able to efficiently show that their code is free of run-time errors (within the degree of soundness of the tools used).

Run-time errors such as out-of-bounds pointer dereference, divide by zero, overflow, and underflow can be detected or proven to be absent using abstract interpretation. The following example below highlights the power of abstract interpretation for code verification.

1 void comp (int *d)
2 {
4 float advance;
5 *d = *d + 1;
6 advance = 1.0/(float)(*d);
8 if (*d < 50)="">
9 comp (d);
11 }
13 void bug_in_recursive (void)
14 {
15 int x;
17 x = 10;
18 comp ( &x );
20 x = -4;
21 comp ( &x );
22 }

In the example above , d is pointer to an integer in the function comp() that is incremented by 1. It is then used as the denominator to determine the value of the variable advance, and after that it is recursively passed to the same function.

Checking whether the division operation at line 6 will cause a division by zero requires an interprocedural verification to determine which values will be passed to the function comp() .

In the code example, two values are passed to the function comp() . When called with 10, *d becomes a monotonic discrete variable increasing from 11 to 49. Line 6 will not result in a division by zero. However, when comp() is called with a value of -4, *d increases from -3 to 49. Eventually, *d will be equal to 0, causing line 6 to return a division by zero.

A simple syntax check will not detect this run-time error. Performing abstract interpretation, as shown in Figure 7 below , proves that all code is free of certain run-time errors except at lines 6 and 21. Note that the function call to comp() succeeds on line 18, but fails on line 21.

Fig 7: PolySpace verification results on interprocedural code.

There is no division by zero when comp() is called on line 18, but a division by zero will occur with the call on line 21 (therefore displayed in orange in indicate failure under some circumstances).

This example illustrates the unique ability of abstract interpretation to perform interprocedural analysis with pointer aliasing to distinguish problematic function calls from acceptable ones.

Improving the Reliability of Medical Devices
Abstract interpretation”based code verification can be applied to improve the quality and reliability of embedded software in medical devices. By employing an exhaustive mathematical proof”based process, abstract interpretation not only detects run-time errors, but also proves the absence of run-time errors in source code.

Traditional verification tools are tuned to find bugs and do not verify the reliability of the remaining code. Abstract interpretation”based code verification makes it possible to identify software code that will or will not cause a software fault.

By using code verification tools early in the development phase, software teams can realize substantial time and cost savings by finding and eliminating run-time errors when they are easiest and cheapest to fix. Because abstract interpretation operates at the source code level, it does not require execution of the software to determine specified coding errors.

Finally, abstract interpretation streamlines the debugging process by identifying the source of run-time errors directly in source code, not just the symptom. The solution eliminates time wasted tracing system crashes and data corruption errors back to the source, as well as time spent attempting to reproduce sporadic bugs.

A code verification solution that includes abstract interpretation can be instrumental in assuring software safety and a good quality process. It is a sound verification process that enables the achievement of high integrity in embedded devices. Regulatory bodies such as the FDA and some segments of industry recognize the value of sound verification principles and are using tools based on these principles.

Jay Abraham is currently Technical Manager at The MathWorks. His area of expertise is in software tools for the verification of critical embedded applications. Paul Jones is a Senior Systems/Software Engineer, and Raoul Jetley is a researcher at the U.S. FDA, Center for Devices and Radiological Health/Office of Science and Engineering Laboratories.

Leave a Reply

This site uses Akismet to reduce spam. Learn how your comment data is processed.