The application of Formal Methods to achieve mathematical guarantees of the absence of undefined behaviors in code has long been the gold standard in embedded mission-critical C and C++ software testing and validation. However, formal methods have also long been associated with complexity and significant expenditures of manual effort.
Embedded systems' complexity intensifies these challenges. Safety (e.g., ISO-26262, DO-178, IEC-61508) and cybersecurity (e.g., ISO/SAE 21434, IEC-62443) testing typically occurs in the late stages of the Software Development Life Cycle when a runnable software version is available.
Formal methods such as abstract interpretation help overcome these limitations allowing developers to shift left in the SDLC by testing earlier and more exhaustively with sound mathematical guarantees of the presence or absence of critical bugs.
During this talk we will review the strengths and limitations of other attempts at comprehensive testing strategies such as boundary testing, fuzzing, static analysis, and dynamic analysis. We will then show how formal methods driven static code analysis can help alleviate some of the most common limitations of those approaches while combining many of their strengths in a complimentary fashion.
We will then finish by looking at a few practical real-world cases highlighting the above and reviewing the resulting cost, time, and quality experienced when leveraging formal methods for specific embedded projects.
