基于模型检测的审计方法逻辑正确性验证  

Verification of Logical Correctness of Audit Methods Based on Model Checking

作　　者：李雅 黄少滨[1] 关晓康 李艳梅[1] 朱璧如 LI Ya HUANG Shaobin GUAN Xiaokang LI Yanmei ZHU Biru(College of Computer Science and Technology, Harbin Engineering University, Harbin 150001, China College of Computer Science and Technology, Jilin University, Changchun 130012, China)

机构地区：[1]哈尔滨工程大学计算机科学与技术学院,哈尔滨150001 [2]吉林大学计算机科学与技术学院,长春130012

出　　处：《吉林大学学报（理学版）》2017年第5期1261-1268,共8页Journal of Jilin University:Science Edition

基　　金：国家自然科学基金(批准号:71272216);国家科技支撑计划项目(批准号:2012BAH08B02)

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

关 键 词：形式化验证 模型检测 审计方法 

分 类 号：TP311.5[自动化与计算机技术—计算机软件与理论]