Model Checking

Estimated time to read: 3 minutes

Overview

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

It checks 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.

One school of thought says that, we can look at our program as a mathematical artifact. And we can prove properties about what the program does.

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.

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

Example

You can express the behaviours that system as state changes.

"It's never the case that I will sell the same ticket to two different customers."

You're saying that before this ticket was sold, the world was in a certain state. After this ticket was sold, the world was in another state. And this other state doesn't have two people holding the same ticket.

At some point in time, ticket A is sold, then at all future states in time, ticket A is only held by exactly one owner.

Model Checking our example

The model checker can then look at the way the system evolves. How does it know that? Well, the model checker has a little bit of an idea of how your program runs. That's a different issue, we'll get to that. But the model checker explores the future and then it comes back with an answer. And the answer's either, yep, it's never the case that two people have purchased the same ticket or it says that's wrong and here's the counter example, here's all the weird steps that the system went through, in order to make it so that customer one and two both hold onto the same ticket.

State Space Explosion

The problem with model checking is the so called stage space explosion.

If you have one bit, you have two states. If you have got I ten bits, I've got two to the tenth states.

If you got 1 million bits, you then have 2 to the 1 million states.

There's no way to explore to the 1 million.

Current model checkers can only extrapolate to around 2 to the 40th states.

That means if your problem can't be described in a small number of bits, the model checker won't help you.

Instead of modelling the entire program, take specific extracts to run against the Model Checker and use those instead.

Deadlocks

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.

State Models

A state model is an abstract state machine that can be in one of various states. The model checker then checks that the state model conforms the certain behavioural properties.

Model Checking phases

Modelling Phase

This is where you enter the model description. This will be provided in whatever programming language your system uses. You also describe the desired properties.

During the modelling phase, you can perform some sanity checks.

These are quick checks that should be easy to do because they usually come from very clear and simple logic.

It's like testing if a light bulb is working by flipping a switch on and off. It's clear to see when the light bulb is malfunctioning.

It's beneficial to get rid of these simpler errors before using any model checkers so that you can focus on specifying the more complex properties to check.

Running Phase

This is when you run the model checker to see how your model conforms to the desired properties that you've wrote in the modelling phase.

Analysis Phase

This is where you check if all the desired properties are satisfied and if any are violated. Violations are called counterexamples. Your model checker will provide descriptions of violations in your system so that you can analyse how it got to that state.