Write Zero-Defect Code: Harnessing the Power of Formal Methods-Based Verification

Thanks, Prashant. So I am Vaishnavi. I am working here as a Senior Application Engineer and mainly focusing on code verification products from The MathWorks and moreso, I think, formal methods-based verification. So we deal with a wide variety of customers who are working in functional safety domains, so spanning from aero to auto semiconductor, medical, et cetera. Yeah. I am also looking forward to have a very fruitful discussion today.

Thank you. All right. So let's understand the context to this discussion. Bugs are bad. That's a known fact, right? We know that, right? But certain bugs are definitely worse than the others. Look at a runtime error, which can get the system that you're creating to fail on the field. Compare that to a coding standard violation. So there is a significant difference between these two. A real field-level failure like this is definitely more catastrophic, loss of money, loss of lives.

Let's, for instance, look at the last case, which is mentioned here about Therac 25. 1980s, we had-- this was a radiation therapy machine. It was supposed to revolutionize the medical devices industry, whereas it set it back by 10 years. It killed six people, fatally injured many more.

And this brought in a context of ensuring that there is more and more checks in a software-defined system These were tested, mind you know. It is not like there was no testing in this at all. Right? With all of this testing, it still went through on to the field, damaging lives or causing serious effect on lives.

So the question really that I'm trying to bring up before both of you today is simply about whether we can add a new step in the entire process itself, or whether we can really complement this process to see if we can add a new step, which avoids issues like this. Is that feasible? What do you wish?

So yes, as we are discussing a lot of advancements, cutting-edge technology, and moving towards modern development phases, software is becoming very complex. And we are adding so many features and all that. But we should also think that when we talk about verification, we also need new techniques, new strategies, because we have to be in pace with the development, right?

So that is where we want to discuss today about formal methods. So you may ask, what is formal methods, right? So formal methods is nothing but it's a mathematical approach, basically. So you are going to be modeling your software in terms of a mathematical model, and you will be proving the correctness of the code, right?

So you are discussing about very critical defects like the raised condition or divide by 0. So many things you put up on the screen, right? So when you talk about this, we are literally going to be proving the correctness of the code, whether such errors are present or not, OK? And in today's discussion, we'll be looking at a specific technique called as abstract interpretation-- I mean, an application of one such technique.

And we have automated this process at MathWorks using a tool called Polyspace. So the Polyspace is nothing but a formal methods engine which is working at the back end and proving the correctness of the code.

Yes, I totally agree to that. So far, you see what you have shown the cases where this could cause failure, right? I think all the techniques, the legacy ones, are more inclined towards finding the bugs. But this which you have mentioned of a formal method, which is based off abstract interpretation, it mostly focus on the code correctness. OK, right?

I think you have actually, you are about of Polyspace, yeah.

So I told you about Polyspace, one of the The MathWorks product under the verification portfolio. So this is basically statically analyzing your code. Be it C or C+ code, we can statically analyze them using the formal methods technique.

Now, for example, on the screen if you can see, there is a code snippet, right? And you see different colored annotations, or it's nothing but an outcome of the analysis from Polyspace. So wherever you would find a red, that means it's a faulty condition, or definitely there is a runtime error.

Prashant was telling about proving, right? And I was also talking about proving. So you got a proof-based analysis of what that red is. That means there is a definite runtime issue, which we have to address. If we look at the software industry, unreachable code or dead code is another big issue.

So while we are statically analyzing the source code itself, we will be able to identify such unreachable zones in the code so that we can optimize our code, or we can look at any logical errors because of which there is a gray code or, sorry, a dead code. And oranges means that there are some possibilities of these runtime errors.

As Prashant was telling that time that most of the time we do things to catch the bugs, but to prove the absence of error I think is one of the biggest ROIs. Even now, I watch for that. And if you look at all the green parts from Polyspace, that means there are no runtime errors. Isn't that wonderful?

Yeah. So I guess the onus on the tool here is about proving that the code is working fine, whereas for testing, it is the other way around to try and find the maximum as possible. So I think it's a different way itself the tool works--

Exactly. Correct. So whenever we look at a typical product development process, so you would see this as the V cycle, right? So all the way spanning from requirement system, requirements to going towards implementation and then doing system integration and calibration. There are so many processes which we see.

So I would like to ask Prashant, so now we have heard a little bit about formal methods. Now how do we actually apply this? Where can we apply in this tool as V diagram if you look at or in our software development processes typically?

Yep, that's a good thing, a good question. And you see that we go through various stages of the software development life cycle. And I'm not going to do the following method by myself. As what you mentioned, we've got a product called Polyspace, and it runs for C/C++. And where the codes are used, typically they are used in software design coding and software integration. These are the stages where the software comes into the picture.

And to make what we're showing there, those colors, what she has shown, I'm going to take three different examples to work you all and show you how a developer can leverage a formal method, a developer or tester can utilize in their testing process or even the integration for that example, how they can see how our modules have been integrated the properly.

And then also whether it's a tester, developer, retailer-- it doesn't matter. But if you are dealing with a coding standard, how do you justify how to identify or justify coding guidelines? Something in this, I'll draw the line. Maybe this is the first demo in which I just play the video and voiceover. Here is a simple code. You can see there is the array of size 5 which typically prints 5 by 5 matrix. I'm using the Visual Studio IDE. Reading the code, as you see that is build parsed.

OK, so we are supposed to see a 5 by 5 matrix as an output, right?

You don't get the output there. And this is where all developers have been there, right?

Yeah.

What went wrong? And typically, when you are dealing with other's code-- the obvious next step is debugging. We're doing the debug, and you can see the debugger open the thing. And I'm going to do step in, step out. And that's the unique added function. Inside that, there is a while loop. And I'm doing multiple step in, step out. But then nothing coming on actually out.

And also, I keep it run for continue. There you go. On the left-hand side, you see the process memory is being consuming. But still, there is no 5 by 5 matrix out. So debugging is good but at a time, it's very time-consuming. Now if I fire formal method, you can say--

So this is the formal methods policy tool?

Yes. I'll just halt a minute because it just went fast. You can see this is the result. I'm not going inside of the tool. But I'll focus only on the results. And you can see already giving me 38% coverage for that code. What does that mean? When my Polyspace entered the main, it did not exit out from the last step. It's stuck in between. So only 38% of the code is in operation, which means there is definitely an issue, right?

And if you go back in the review, there is a red check as you've shown in the previous slide. See there, it's showing non-terminating loop for the while loop? Even in the debugger, we were doing it. But what is important here is highlighting the gray part, that if condition showing the dead code. What is a conditional loop. There is one calling a function, which is always returning 0.

The tool tip, I love the most. Because inside this member queue also, there is a for loop. And what does it show? Unreachable code. Because the condition is false, 0 less than 0 is actually the cause.

So you can see that range, right? You can see that left-hand side is 0, right-hand side was 0.

There you go. See, even from the first Q2, the caller to Poly, right? How the argument passed and their ranges. And though that for condition is false, the member queues are returning 0. And because of which the counter was not updated. And hence, the code was always stuck in the while. And that's the whole reason why we were stuck. Right? Let's go back and change in the code and rebuild it.

And--

We should hold on.

--I think I've seen the whole thing.

So Debbie, yeah, you saw that in the window, right? There were a couple of other results. So we don't see any outcome. So there is a second run. But here, you see 43%.

This is after--

Earlier, we have--

--you corrected the code, right?

Yes.

Yeah.

The problem persists, but we made some more line counter.

Counter.

Right? For example, you see now the if for loop is reachable. But below at 48, there is a uninitialized variable. That array of i. And because OK, and on the left-hand side bottom, we can see here the trace. So if I click there on the right-hand side, it shows array is declared within the main, which is passed to unique randint function as the third parameter. This is unique. You need to map .

Yeah. I think we have enough clues for the developer to actually deal with it.

Yeah. But what is the big thing here is I don't know. I ran with the default option's ID. ID would have shown me this, right? It did not show me. This is the trick. Right? And now I'm going to build it. Hold on. So this is what you were expecting, right? So I'm just reading plain. I'm not doing any calculation, just an empty buffer we are reading it.

Right.

But now you can see setup. As you said rightly, the code correctness. This exactly is not more about proving. It's more about the code correctness.

The faster is the processing working with this code as well.

Yes.

And this is expected in let's say. Let's look finding the issue fastest and getting the solution. I think a tool like this one.

Yeah, one which, in this example we talk, shown, is not a bug. It's more of a-- do with the logical error.

Yes. Yeah, so I think-- so in the demo, what you showed, Prashant-- so do you agree with these things? So first of all, I think you were showing a lot of unreachable code. So it's a very nice way that we can actually refactor the code. And two things, second, what you already mentioned, of course, we did find some logical errors.

Yep.

First thing is to find them. Second thing is it already ignored you. It gave enough clues. Or it actually leads us to understand the root cause better.

Yeah.

So I think we very much can see that in this demonstration, that I agree with all these three factors. Do you?

I totally agree. So this makes the developer's life so easy.

Yeah.

Sometimes, you write your own code. Sometimes, you work on the legacy code, which you don't know the whole dependency structure, swap tracing.

Right.

And debugging for small code, in this example, we took very small code. It's fine. But in real world, you know.

Yes.

Many times, debugging is frustrating. Then the next thing, what I'm going to show you from a testing point, now, developers want to do some tests. For example, let's say for example, in this example, there are two files. test_harness, of course, has the test drivers in it. And there are errors on my unit under test.

In my Visual Studio code, you can see here I have written test drivers for loops, and passing it a function new position, and passing the argument minus under 2 plus 100 to this new position, which takes position 1, position 2 as two arguments. And then, there is a pass and fail criteria. Other test case, I have commented. And typically, this comes from your requirement specs.

Right.

This is more of a functional test. I'm compiling this code. And let's run. One good thing you obviously see here is all test cases are passed.

Yeah, that means .

Yeah, just hold on a minute. But here, you see all have passed. But also, you see my plus 8 to minus 8. And for other values of i and j, it is 0. But what wonders me is when I see the definition of the function, I don't see the intrinsic of the function, anything at all. Whereas, this is a Polyspace tool. I applied the formal methods. And let's go to this test driver first. And you can see the tooltip, which I talked in the previous demo--

Oh, OK. Correct.

--showing minus and then plus minus.

So already, it is showing.

Yeah.

Yeah.

This is the main important take. You see here, you see all green in each statement. You can typically see actual position, which is a local variable, ran increment to date. And the e connection is shown as always true. So if these are my inputs, that if condition is redundant. So this is where I can understand this part of the code and remove that e, make code much more smaller or complex.

Yeah, and it's no more a black box.

Yeah.

So in this testing, we can actually get exposure to the code as well.

In the second module, what I'm doing here, do I need test drivers? I don't. The same file, I just--

Yeah, you are just using the unit under test.

Yes. And I'm just running it. So by default, it takes the full range. For example, if you open the results in position 1 and position 2, consider a full int32 range.

So you have not driven any inputs here.

And then, this time the e ranges of position 1 and position 2, the e becomes false.

Oh, OK. So it's more or less like the robustness.

This is a robustness. And you see there, everything is green. And it gives me 100% guarantee, confidence. And another way, if I had to test my way, so we call constraint setup. So what it brings up, it lists out all my global variables, user-defined functions, and step functions. In this case, we have only user-defined function. That is new position. For each input, rather writing test drivers, I'm specifying my own limit. Position one was minus 2,000 plus 1,000. Second argument was minus 252 plus 500. And we can run this. So you see this is my specified range.

Correct.

And what is the output without test case, without writing the code, without executing the code?

Right.

So I think the code is there. But it's [AUDIO OUT].

Yeah.

Sorry for that. But yeah, so this is how I can minimize with the testing. Even developers can use in their test development-driven approaches.

Right.

Which is coming [AUDIO OUT].

Yes. I think that was indeed a very great demonstration. We really did not develop test cases. We could get inside the code, get in our insights into what the code is actually looking like in terms of correctness.

Yes.

And I think this is-- in a way, it will be a very efficient way to complement our testing, Prashant, whether it is unit or integration. And also, I think you also showed that you are running that entire code base with all the input values. And every statement being covered, that means every flow was covered. That is equivalent to robustness.

Exactly. And sometime, in my experience, the customers also, some of the lucky ones, also told me that with using this approach, they could also review the test cases. Have they written exhaustive test case, efficient test case? So this definitely adds some value.

And I guess this even touches the boundary condition, everything, which test modules might miss out on.

Yes. Yeah, so for example, it was what case studies we presented. They must not have tested for all the ranges.

True.

So this is what, at least, you can make use of.

All right.

So the next one, as you mentioned, about the coding guidelines.

Yeah.

But here, I'm going to take model design as one approach, just to show you in NVIDIA how it works.

Yeah.

But for formal method, it just works on CC++. So it doesn't matter whether it's coming from an auto code or a hand code. It doesn't matter, that one.

Right. Many customers, actually, these coding standards being one important aspect. I think many customers spend a lot of hours in terms of going through how many violations with-- at least, those violations has to be actually addressed. Or they can be justified. So this is, I think, eats up a big chunk of activity from our engineers. So yeah, if you can demonstrate that, it will be really great.

Yeah, it reminds me of my startup early days. When I started, I used to sit alone with my teammates. And we projected in our big screen. And then manually, we were walking through what's wrong and then-- but thanks to these, that we have tools like these.

Yeah, I think there is always a constant argument between developers that--

Yeah, they are.

That's not a fun part, definitely. That's not a fun-- to be there. But yeah, coming back to this demo, what I'm showing here, this is a Simulink model. Let's say I'm taking an auto code as an example. So this is a Simulink diagram where you have a closed loop. This is the controller [AUDIO OUT] Here is the reference model.

Right.

And controller is the one where you go and generate the code. And here is the code. On the left-hand side, it's shown.

So the code is already being generated, has already generated.

Yeah, but you see the Polyspace just right and go and sits in the Simulink.

Oh, exactly.

Yeah, exactly.

Yeah.

So I'm just setting up basic. Or I'm setting it for MISRA-C 2012 compliance, and along with a method-based [AUDIO OUT] as to how it complements our coding guidelines. So what I'll-- we can see in this next, we'll fire up the Polyspace within Simulink. That's just a click of run. And you see [AUDIO OUT].

Yeah, so you haven't supplied any source code or anything. It has just picked up everything from Simulink.

Yeah, that's the whole point. In NVIDIA, you have to stick within MATLAB Simulink.

Right.

You don't want to go out of the environment. So this vacillates. We can see all these generated code being taken care of. But what else, also, you see is in the model at the design level, you specified some min/max ranges.

Yeah.

From a modeling perspective, all that is taken care into account. This Polyspace window opens up. And you can see, for example, encoding standards, rule number 12, it's showing 13 violations. And in the violation 12.1, typically, it talks about precedence of the operators. But what you notice there-- and well, you see the green color. You know, you understand green color. So that's the MISRA violation. It's an advisory, though, for an example. But there is an overflow check which says that it is safe to have that check.

Oh, so--

[INTERPOSING VOICES]

Yeah, it means that even though there is a MISRA violation, I can justify directly. And I can say there is no workflow because Code Prover is telling me?

Yes, Code Prover has proven it. I can take that justification. And as it is a model, just as to answer your question, I'm using that hyperlink to trace it back to the model. If it's in a submission block, you can see.

Right.

And there's an entry multiplied by that input. And then, plus adding 100 and checking condition is greater than 43 or not. So I just right there in the Simulink go and annotate that block.

This is within Simulink?

This is now within Simulink. Yeah, so you can select MISRA-C:2012, rule number 12.1, and the status justified, something like that. Severity, Low. For comment, demo as just an example. And then Apply, OK, and save the model.

So my designers know that there is some annotation over there.

Some Polyspace annotation exist.

Yeah.

Because that's for model point, it's all right. But in code, there is a violation. But Polyspace has at least proven that violation is OK. So if the same developer or if you pass this model to somebody else, and if they generate the code and rerun the Polyspace, you will see the magic now.

Oh, does it mean that-- then I'll still get the violation. I need to redo this thing?

No, that's the point. If you annotate at the model level, the model is your reference thing.

Right.

So if I redo this stuff, [AUDIO OUT] shown 13 violation, you remember that? Now you see there is a 12 violate which are now 11 because the two violations to that operator have been suppressed. Or it's showing that it is being justified.

Oh, that's great because we don't have to redo this--

[INTERPOSING VOICES]

--once.

Now, in this example, I did it for the model level because I was just showing you one example, how it is integrated with NVIDIA. The same thing, if you are not doing NVIDIA, if you are doing a hand code, you can still do this annotation in the source code level so your annotation exists as comments in the code itself.

But throughout the code life, it will be there. So that even if I run in any projects, I don't have to revisit that.

Yeah, exactly.

That's great.

There are various ways of managing it. But yeah, but the bottom line is here, I can leverage formal method to justify hard to understand some of these coding guidelines.

It is also quite exciting that [AUDIO OUT] autogenerated code and hand written.

Yeah.

Polyspace considers everything the same, doesn't it?

So basically, we need CC++. So it doesn't matter from where. Only in NVIDIA, it adds an additional step, is you can have a traceback.

True.

Yeah, I think what I personally liked is the Simulink integration, though our final objective is to justify the coding rules. But I think if you-- if we are in the NVIDIA platform, then running a Polyspace is no additional activity. It is just click of a button. And then, we can trace it back. So I think that's a very seamless step. But yes, however, the main objective, what we are solving for our developers, is hard to justify coding guidelines. I think that was really fantastic.

So moving on, yeah, these are the three quick demos, I think. But if you have questions, so you guys can pop the question. I think the attendees who have been watching us, they can put it in the Q&A. We can take it up.

Yeah, and if you have heard us today in our discussion, so we have talked about some of the benefits of formal methods. And it's not just we're discussing. But even if you look at our customer portfolio over here, you can look a wide variety of customers. So we can see some customers in the automotive segment using Polyspace. We can see aerospace, where they have already complied to DO-178. Then you can see medical. You can see others. Even, you can see railway. Plus, you can also see Miele, which is, again, medical-- sorry, home appliances. So I think that's where the mass production is. [LAUGHS]

We are very stateside because they produce in billions of units.

Yeah, exactly.

And one small product can cause such .

Yeah, just imagine if my dishwasher didn't do what it had to do.

[LAUGHTER]

Yeah.

And I think it's about caring for the customers, caring for your products.

Yeah.

Simple as that.

Billions of the dishwashers have to be recalled. Anyway, so coming back to the discussion, so it is not just, we have seen a wide variety of our customers who have been using formal methods-based approach in their verification. So if we look at-- specifically, I would like to say this to Amal, actually. He brought about the topic of Therac-25, the medical appliance.

So now, look at this. This is Miracor. This is, again, a medical appliance company. And if you look at what they are actually working on, it is a Class III medical device. So if you even note, it's improvising outcomes for stent recipients. So you know how critical this could be. And they have used Polyspace, Code Prover. That is the formal methods-based tool. And like how we were discussing unused code, which we were largely focusing how we can actually tackle them.

And then, what they look at is the regulatory body, FDA, which is very stringent, correct. And Miracor was able to satisfy them, at least looking at they are producing stuff. And then, they have to take safety things from FDA. Then they were really able to satisfy that. And their code reviews have improved and all that.

[INTERPOSING VOICES]

--efficiency improving is a big factor. I think in the modern world, the best way you can do something, the most efficient way you can do something, it's something that you adopt.

What you see there, Amal, I like that [AUDIO OUT]. It helps [AUDIO OUT] but not only demo quality, but also the correctness.

[INTERPOSING VOICES]

So I think it's very exciting looking at the breadth of the industries that this tool is able to cover. In a way, I can even say it's agnostic. But at the same time, that means a wider coverage. And look at the latest applications, even ADAS, or even very critical applications like medical devices software. It's really exciting. And thank you, Prashant, thank you, Vaishnavi, for allowing-- allotting your time today for this. And thank you. And take care.