Embedded Toolbox: Prove It! Proofs Start Where Static Analysis Stops

February 25, 2021

Blog

 

Static analysis tools are widely used in safety- and security-critical applications as a means of finding and remediating coding errors. In fact, they are the de facto software testing tool in these industries.

Of course, static analysis is not the end-all, be-all of QA tools, nor is it a perfect solution by any stretch of the imagination. It is particularly adept at going through a codebase line-by-line and isolating potential errors, which are usually fairly simple, and providing a list of messages or alerts as to their possible cause. But there is another layer of analysis that can and often must be performed in order for developers to remediate bugs quickly and effectively.

And we're not talking about dynamic analysis. We're talking about proofs. When you need guarantees, rather than suggesting the possibility that they could exist and affect code operation in some way, proofs will prove that there aren't any errors. This can be applied to divide by zeros, buffer overflows, and a host of other bugs.

Building on a previous Embedded Toolbox where his colleague Rob Tice, used the CodePeer static analysis tool to address errors in the code of a Zumo robot, Yannick Moy, AdaCore's SPARK Product Manager, demonstrates how the SPARK language can be leveraged beyond static analysis to perform proofs natively during the software development process. This not only helps reach those elusive, extremely high double digit code coverage numbers, but also saves time and money on the backend.

Are you ready to prove how reliable your code is? Tune in and learn how.

TECH WAGER: If you find any bugs in the Github repo below, resolve them with SPARK proofs (tutorials and background information also available below), and screenshot/record your work, we will send you a FREE Zumo bot!

• SPARKZumo Github Repo: https://github.com/Robert-Tice/SPARKZumo​

• Intro to SPARK and Proofs: https://learn.adacore.com/courses/int...​

• Zumo Robot Prize: https://www.adafruit.com/product/1639...​

• Contact for Questions, to Submit Your Work: Brandon Lewis, Editor-in-Chief, Embedded Computing Design ([email protected])