3.8 – Model Checking

3.8 – Model Checking

 

Model checking is a systematic check of your system's state model in all its possible states. 

Basically, you check all the various states of your software and find that there are any errors by simulating different events that would change the states and variables of your software.

 

 

What is model checking?

If you can express your problem that way, then you can do what's called model checking. And model checking is a technique that does state exploration, it says, given that you start in this current state, explore all the possible ways you can go into the future and reason about what all those possible future states can look like.

 

What are issues with model checking?

The problem with model checking is the so called stage space explosion. If I have got one bit, i have two states. If I got I've got ten bits, I've got two to the tenth states. If I have got 1 million bits, I've 2 to the 1 million states. There's no way to explore to the 1 million. Current model checkers last time I knew anything about them, were about 2 to the 40th states, was about the most you could explore.

 

What assumption does model checking depend on?

So model checking relies on this thing that we call the small world assumption. That, if you have a system and 

things are going to go wrong, they're going to go wrong in small cases. And that if you look at the small cases, you can convince yourself to a reasonable degree of confidence that it is probably going to work in the big cases. That is the program extraction part, that's still a big problem, no one knows how to do that well. There is lots of tools that are good partial solutions but there is no general solutions to that.

 

How does model checking fit into verifying software?

Model checking and listening over a programs and Azure development and test cases, they all fit together very nicely, because if you can specify what your system does, you can write test for it. In some sense, test are themselves specifications. Because if you pass it, it is doing the right thing, if you do not pass it, it is doing the wrong thing. 

If you can model check your system, that is good, because it means that you have some specifications that do not need test cases. Because the system is actually correct.

 

What software systems can benefit from model checking?

It is only a small percentage of all the code that is written that can actually benefit from model checking because either it is not important enough who and you do not care who do the investment, or it is simply too complicated and model checking is not powerful enough yet.

 

 

Model Checking Explanation with an Example

Think of model checking like going through airport security. Security guards in airports know the rules of what people should have or should not have to get on an airplane. They do not make any exceptions. Model checking is similar and that it checks the behavior in the state model for your system and notifies you of any violations to the rules. A rule that your software is required to satisfy is it must not produce a deadlock. A deadlock is a situation where your system cannot continue because two tasks are waiting for the same resource. Your model checker would simulate the different states that could occur in your system and if a deadlock is possible, it would provide details of the violation.