How Static Analysis Supports DO-178C Verification

Developing software for airborne systems requires strong verification evidence, especially for higher-criticality applications. DO-178C defines objectives for airborne software development and verification, while DO-333 provides guidance for using formal methods as part of that process.

Static analysis tools such as Astrée, aiT, StackAnalyzer, and RuleChecker can support several of these verification activities and help reduce the amount of manual effort required during certification.

Where Static Analysis Helps

Testing is essential, but some properties are difficult to demonstrate through testing alone. For example, proving that all relevant program paths and hardware conditions have been exercised can require significant effort.

Sound static analysis based on Abstract Interpretation takes a different approach. Instead of relying on individual test executions, it analyzes an approximation of all possible program behaviors while keeping the result on the safe side.

DO-333 recognizes Abstract Interpretation as a formal method, and AbsInt maps its analysis tools to several DO-178C/DO-333 verification objectives.

The tools address different areas of verification:

• Astrée detects potential runtime errors such as overflows, invalid pointers, uninitialized variables, array access errors, and data-flow issues.
• aiT determines safe upper bounds for Worst-Case Execution Time (WCET).
• StackAnalyzer determines safe upper bounds for maximum stack usage.
• RuleChecker checks compliance with coding guidelines such as MISRA and other supported standards.

Together, these tools can provide verification evidence for runtime behavior, timing, memory usage, control/data flow, and coding-standard compliance.

Where the ROI Comes From

The ROI is mainly found in two areas.

First, static analysis can reduce verification effort. Determining WCET or stack usage through measurement may require extensive target testing and confidence that the worst-case program and hardware conditions were actually observed. Sound static analysis provides safe upper bounds by design, reducing dependence on exhaustive testing.

Second, there is tool qualification effort. When verification tools are used to reduce or replace manual verification activities, qualification requirements may apply under DO-178C/DO-330. AbsInt provides Qualification Support Kits for aiT, Astrée, and StackAnalyzer to support this process and reduce the amount of qualification material a development team must create themselves.

Bringing Verification Earlier into Development

Static analysis is most valuable when it is used throughout development rather than only at the end of the certification process.

Running these analyses early can help identify runtime errors, timing violations, stack problems, and coding-standard issues before they become expensive integration or certification problems.

For teams working toward DO-178C compliance, static analysis therefore provides more than defect detection. It can become part of the verification strategy itself helping improve confidence in the software while reducing verification and qualification effort.

Want to learn how these tools fit into a practical DO-178C workflow? Join us at our upcoming in-person event to explore how static analysis can support safety-critical software development and verification.