A Model Checking Example: Solving Sudoku Using Simulink Design Verifier

Formal verification methods prove mathematically that a design does not contain unwanted behavior. As a result, they help ensure that a system design meets the specification before time and effort are invested in implementation.

In this paper, Walter Storm, a senior developer at Lockheed Martin, presents an easy-to-understand application of formal methods—specifically, model checking.  Through an example based on the popular game Sudoku, Storm demonstrates the power and simplicity of model checking technology as implemented within Simulink.  Topics covered include formalizing constraints and requirements, using math to search for solutions that prove design correctness, generating counterexamples (test cases known to violate the requirements), and fixing these violations.