2 Coding Examples of How Formal Methods Improves Testing for Safety-Critical Software
November 7, 2024
Formal Methods-Based Testing Key Points
- Unlike traditional verification techniques, formal methods can provide 100% coverage of all legitimate inputs
- Formal methods-based verification tools that account for a software unit’s context significantly reduce false positives
- Advanced formal methods-based verification tools improve test efficiency by reducing the input state space
Introduction
Verification of safety-critical software has reached the limits of traditional testing techniques. As software complexity grows, so does the need for a more reliable verification approach that accounts for complicated input and control paths through code. Current static application testing, dynamic simulation, and similar methods fall short of exhaustive bug detection throughout an application’s state space. This limits developers’ ability to provide complete assurance that safety and vulnerability issues have been mitigated, causing risks to compliance and delivery.
Formal methods offers a better mechanism to support the verification needs of modern safety-critical software development. As a set of mathematically rigorous techniques implemented by highly optimized algorithms, formal methods helps developers prove the correctness of their code with absolute certainty. Unlike conventional approaches, formal methods offer a soundness guarantee, enabling the detection and elimination of 100% of undefined behaviors—such as buffer overflows, uninitialized memory access, and arithmetic overflows—that could pose serious embedded cybersecurity, safety, and reliability risks.
This blog explains how formal methods-based verification improves upon traditional techniques through two practical code examples using the TrustInSoft Analyzer exhaustive static analysis tool.
Formal Methods vs. Traditional Verification Techniques
Before walking through the code examples, here is a short summary of why a formal methods-based static analysis tool improves safety-critical software testing:
- 100% coverage of all legitimate inputs, ensuring greater confidence that the application’s state space is sufficiently covered to meet common industry standards such as ISO 26262.
- A soundness guarantee where no error is missed, resulting in zero false negatives, and every finding is provable through mathematically rigorous techniques.
- The elimination of issues early in the software development lifecycle. As Figure 1 illustrates, running a static analysis tool based on mathematically sound formal methods earlier helps find and eliminate issues using less time and budget than during later phases.
Figure 1: Lifecycle effort comparison between traditional testing and TrustInSoft Analyzer
Here are two examples of how software verification using formal methods differs from traditional techniques.
Example 1: A Divide by Zero That Never Happens
A divide-by-zero error can be catastrophic to program behavior, such as the potential issue caused by this code:
int f(int a) {
if (a > 0) {
return a/0;
} else {
return 2/a;
}
}
Traditional test methods would likely catch that the statement return 2/a; may cause a divide-by-zero error depending on the value of a passed to the function f().
Consider the following code sample:
int g(int a) {
if (a >= 0) {
return 0;
} else {
return f(a);
}
}
If this function g() is the only function calling f() in the entire application, the statement return 2/a; is never executed, meaning a divide-by-zero will never occur.
Rather than understand this subtle difference, most traditional static analyzers would report a potential divide-by-zero error and add to the number of false positives that a developer must review and address. A formal methods-based tool, given its soundness guarantee and exhaustive bug detection, is fully aware of the context surrounding each unit under test and would not report such an error. This reduces the number of false positives and avoids wasted effort.
Example 2: Exhaustive 32-bit Integer Testing Without Billions of Test Runs
Consider this function:
int P(int data) { return data + 1; }
Assuming a 32-bit processor architecture, a test case that covers all possible inputs into the function P() would have to run through over 4.3 billion integer values. Creating and executing such a test would be far beyond the scope of most development resources, so teams usually take a sporadic, “worst-case inputs” approach that skips a significant portion of the actual control and data paths.
Using advanced Input Coverage Reporting, TrustInSoft leverages the mathematical notations used in formal methods to reduce the set of all possible values into an interval definition. For function P(), this definition looks like:
“-2,147,483,648 <= data <= 2,147,483,647”
TrustInSoft Analyzer uses this compact representation of P()’s input state space to verify that the function gives the expected result for every memory layout and entry value:
- Allowable input: -2,147,483,648 <= data <= 2,147,483,647
- Predicted mathematical output (incremented by 1): -2,147,483,647 <= data <= 2,147,483,648
Detecting potential issues requires only two mathematical operations: incrementing the lower and upper bounds by one. For example, a predicted mathematical value of 2,147,483,648 is invalid for a 32-bit integer, and a signed overflow must be reported.
Rather than billions of test runs, this reduced set allows developers to test exhaustively in less time and prove that legitimate inputs always result in legitimate outputs – a key mechanism in supporting ISO 26262 compliance.
Conclusion
Formal methods is having a profound impact on the verification of safety-critical software, offering a level of exhaustive bug detection and assurance that traditional methods cannot match. By proving the correctness of code and guaranteeing the detection of all possible errors, it provides a powerful tool for developers to ensure the safety, security, and reliability of software.
For more examples and a deeper understanding of how formal methods improves critical software testing: Learn more about TrustInSoft Analyzer