摘要
利用模型检测的建模方法,对审计方法及其计算过程和期望的计算结果进行建模,并在模型检测器上对逻辑性较强的凭证断号检查审计方法进行验证,提出一个利用模型检测方法对审计方法逻辑正确性验证的框架.利用模型检测器给出的反例,对验证的审计方法进行修正.实验结果表明,模型检测方法能验证审计方法逻辑的正确性.
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.
作者
李雅
黄少滨
关晓康
李艳梅
朱璧如
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)
出处
《吉林大学学报(理学版)》
CAS
CSCD
北大核心
2017年第5期1261-1268,共8页
Journal of Jilin University:Science Edition
基金
国家自然科学基金(批准号:71272216)
国家科技支撑计划项目(批准号:2012BAH08B02)
关键词
形式化验证
模型检测
审计方法
formal verification
model checking
audit method