Abstract: Using the modeling method in model checking, the audit method, its calculation process and the expected calculation results were built to a model, and the audit method of voucher number checking which had strong logic was verified using model checker, we proposed a framework of using model checking method to verify the logic correctness of the audit method. The verification of the audit method was modified by using the counterexample of the model checker. The experimental results show that model checking method can verify the logical correctness of audit methods.

Key words: audit method, formal verification, model checking