中文摘要：

利用模型检测的建模方法,对审计方法及其计算过程和期望的计算结果进行建模,并在模型检测器上对逻辑性较强的凭证断号检查审计方法进行验证,提出一个利用模型检测方法对审计方法逻辑正确性验证的框架.利用模型检测器给出的反例,对验证的审计方法进行修正.实验结果表明,模型检测方法能验证审计方法逻辑的正确性.

英文摘要：

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.