How to make sure the system that you’ve created is correct?
For example, you can run tests and see if the actual behavior matches what you expect. But there is another technique called model checking.
Model Checking is a systematic check of your systems state model in all its possible states, can help to find laws. Its done after code has been written and before deployment.
How to model check software? Model checkers generate a State Model from your code.
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 to certain behavioral properties.
There are 3 different phases to performing model checking:
- The Modeling phase – this is where you enter the model description and describe the desired properties.
- The Running phase – can see how your model conforms to the desired properties that has been wrote in the modeling phase.
- The Analysis phase – checks if all the desired properties are satisfied and if any are violated. Violations are called Counterexamples. Also you can analyze how you got this state using the information from the model checker with advice where to fix. And then run the phases again until eliminate the issues.
Ivan's Blog 