How Formal Methods Improves The Verification Of Safety-Critical Systems

Formal Methods Key Points:

• Formal methods are mathematical techniques used to prove the correctness of real software systems
• Among other criteria, these techniques prove software determinism, reduce the number of false negatives and false positives in testing, and improve testing confidence by taking hardware characteristics into account (e.g., endianness and size of integer types)
• The result of formal methods-based verification is more robust software, more efficient testing, and improved embedded cybersecurity for safety-critical systems

Introduction

Traditional verification methods cannot keep up with increasingly complex software that must be connected, secure, autonomous, and adaptable to other trends driving the industry. Formal methods-based verification tools change how developers test safety-critical software and achieve standards compliance by proving properties of code using exhaustive and efficient algorithms.

The results of a recent TrustInSoft study, shown in Table 1, show that software verification activities can account for up to 40% of overall project effort for automotive applications following the ISO 26262 certification process. The challenge for OEMs, suppliers, and new market entrants is clear: ensuring their software meets functional safety and embedded cybersecurity standards without increasing overall test effort.

Table 1: Percentage split between development activities for ISO 26262-compliant automotive projects (source: TrustInSoft)

Formal methods techniques give developers 100% confidence that their code has been verified and reduces the effort of exhaustively covering all possible interactions between a software unit and its environment.

What Are Formal Methods?

Formal methods are mathematically rigorous techniques that allow developers to prove their software behaves exactly as intended, eliminating the guesswork associated with traditional testing approaches. They operate on precise mathematical models of the software that enable every step of the verification process to be algorithmically checked and provide assurance beyond conventional testing.

One advantage of formal methods is its soundness guarantee. This ensures that no error goes undetected (zero false negatives) and that every issue found can be mathematically proven to exist. This level of precision and reliability is crucial when developing software that cannot afford to fail.

In safety-critical industries such as aerospace, automotive, nuclear, and rail, formal methods have become increasingly indispensable. By enabling the detection and elimination of 100% of undefined behaviors—such as buffer overflows, uninitialized memory access, and arithmetic overflows—formal methods address risks that other techniques miss and support certification to standards such as ISO 26262 and CERT-C.

The following sections illustrate three ways safety-critical developers use formal methods as applied to static analysis tools such as TrustInSoft Analyzer.

Formal Methods Help Prove Determinism

Formal methods enable an exhaustive and efficient state space exploration of a given unit under test and prove that the unit’s outputs solely depend on its inputs. This rigor makes proving determinism easier and reduces the likelihood of undefined behaviors, such as those caused by incomplete code coverage, occurring in the field.

Consider this statement:

unsigned long after = 10UL + (unsigned long) &G;

Depending on how the compiler allocates memory for G, this statement may cause nondeterministic behaviors when linked to other components and compiled for a specific hardware target.

Traditional static analysis tools may miss this issue as they aren’t aware of the actual target hardware characteristics. A formal methods-based tool like TrustInSoft Analyzer would raise the potential issue as it knows hardware-specific memory layout.

Reducing False Negatives and False Positives in Static Analysis Tools

Traditional static analysis tools often generate a flood of results — some of which are inaccurate or irrelevant. False negatives, where real issues go undetected, can lead to critical issues slipping through the cracks. False positives raise potential problems that don’t exist, consuming valuable time and resources as developers sift through and dismiss them.

The soundness guarantee of formal methods is a key factor in eliminating false negatives, ensuring exhaustive bug detection where all potential issues are identified. Similarly, the precision of the mathematically rigorous techniques employed by formal methods significantly reduces the number of false positives for a given unit under test. Figure 2 illustrates the difference between sound and unsound analysis methods.

Figure 2: Comparison of unsound vs. sound analysis methods

Software Testing That Accounts for Hardware Specifics

Conventional static analysis tools often lack visibility into hardware-specific characteristics influencing software behavior. Consider the differences between 32-bit and 64-bit systems, where data alignment rules vary. In a 32-bit environment using ILP32, the int, long, and pointer types are all 32 bits in length. On a 64-bit system using LP64,long and pointer types are 64 bits, while int remains 32 bits. Without hardware awareness, a static analysis tool might miss these differences and produce false conclusions about software behavior across different platforms, even when the application code remains unchanged.

A formal methods-based tool like TrustInSoft Analyzer takes hardware specifics into account – including endianness, padding, memory map configuration, memory alignment, and integer type size – to help avoid these misleading results when analyzing code.

Conclusion

Developers using formal methods-based verification tools can identify and address potential issues that less sophisticated tools might otherwise miss. In safety-critical applications, where determinism, code coverage, and exhaustive bug detection matter, combining formal methods with hardware awareness in static analysis is not just beneficial—it’s essential. It allows developers to create software aligned with its target operational environment and increases confidence that safety, security, and performance requirements are achieved.

Qualified as an ISO 26262–compliant tool, TrustInSoft Analyzer guarantees no undefined behaviors in code and reduces compliance effort by bringing the accessible power of formal methods to development teams.

For a deeper understanding and code samples explaining how formal methods improves critical software testing: Learn more about TrustInSoft Analyzer