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

吉林大学学报(理学版)

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

李雅¹, 黄少滨¹, 关晓康¹, 李艳梅¹, 朱璧如²

1. 哈尔滨工程大学计算机科学与技术学院, 哈尔滨 150001; 2. 吉林大学计算机科学与技术学院, 长春 130012

收稿日期:2016-07-15 出版日期:2017-09-26 发布日期:2017-09-26
通讯作者: 黄少滨 E-mail:huangshaobin@hrbeu.edu.cn

Verification of Logical Correctness of Audit Methods Based on Model Checking

LI Ya¹, HUANG Shaobin¹, GUAN Xiaokang¹, LI Yanmei¹, ZHU Biru²

1. College of Computer Science and Technology, Harbin Engineering University, Harbin 150001, China;2. College of Computer Science and Technology, Jilin University, Changchun 130012, China

Received:2016-07-15 Online:2017-09-26 Published:2017-09-26
Contact: HUANG Shaobin E-mail:huangshaobin@hrbeu.edu.cn

摘要/Abstract

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

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

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

中图分类号:

TP311.5

李雅, 黄少滨, 关晓康, 李艳梅, 朱璧如. 基于模型检测的审计方法逻辑正确性验证[J]. 吉林大学学报(理学版), 2017, 55(05): 1261-1268.

LI Ya, HUANG Shaobin, GUAN Xiaokang, LI Yanmei, ZHU Biru. Verification of Logical Correctness of Audit Methods Based on Model Checking[J]. Journal of Jilin University Science Edition, 2017, 55(05): 1261-1268.

[1]	黄宏涛, 黄少滨, 陈志远, 张涛. 基于克雷格插值的反例理解方法[J]. J4, 2013, 51(01): 94-100.
[2]	廉智超, 欧阳丹彤. 基于模型检测的实时模型诊断方法[J]. J4, 2007, 45(06): 948-952.