Model checking
Formal verification · automatic state exploration
created · updated
A method in which a program automatically walks the states of a described system and checks that the rules hold in each of them. If a rule breaks, the method outputs the exact chain of steps that leads there. For example, a shop model finds the move “payment, connection lost” after which the money is charged but there is no order: the buyer paid and got nothing. Unlike a test, the method is not limited to scenarios a person thought of, but it is limited by the size of the chosen world.
Source: Wikipedia: Model checking
Read more: Finding races and lost data with Quint models
Where it appears · 4
- Vitest vs Jest · Specs and context
- How to find a race condition in code · Specs and context
- How model checking differs from testing · Specs and context
- TLA+ vs Alloy vs Quint · Specs and context