Formal Verification

By Dr. Jacob Boender, Formal Verification Engineer at HENSOLDT Cyber GmbH

One of the specialties of HENSOLDT Cyber is *formal verification*. This may sound very sophisticated, but what is it exactly? In this blog, we will endeavor to explain. In general, whenever we write a computer program, we would like it to behave exactly the way we want it to. But how to be sure? Generally, the way software developers do this is by *testing*; running a program under specific circumstances and checking that it then does the right thing.

However, testing is not entirely foolproof. The main drawback is that it is only run on a limited number of test cases: if you do not include a particular test case, any bugs that test case might reveal will only show up when your program is actually in use (with dire consequences ensuing…)

The approach of formal verification is different: we use mathematical methods (either automatic, such as model checking, or manual, like interactive theorem proving) to *prove* properties of the program, for example that its output is what we expect it to be, or that it doesn’t keep running forever. Since we’re checking properties of the program as a whole, we’re not dependent on whether we’ve covered everything with test cases.

Of course, formal verification is not perfect either: since we are reasoning about the program, we must have some sort of idea of how it behaves—in other words, we need to have a mathematical model of the programming language our program is written in. And if this model is different from how the program behaves on a real machine, errors might still occur.

So, while formal verification cannot replace testing, it does offer another way of checking a program for errors that is highly complementary to testing. And therefore, it allows you to be more confident about the correctness of your program – and that’s what it’s all about in the end!

Share on facebook
Share on linkedin
Share on email

1 thought on “Formal Verification”

  1. Thanks for the insight, I would appreciate a follow up blog post describing your approach to formal verification. Are you using Cogent for instance or some other methods, and what is your experience with the different methods. Are any particular components of TRENTOS-M easier to verify?. If so, which and why?

    Spark/Ada is another approach to formal verification that could be of interest for user applications as Spark/Ada is a very well integrated solution. Maybe they have complementary uses?

Leave a Reply

Your email address will not be published. Required fields are marked *