模型检测在完整性形式化验证中的应用研究-计算机工程与应用.pdfVIP

Computer Engineering and Applications 计算机工程与应用 2017 ，53（4 ） 59 模型检测在完整性形式化验证中的应用研究 严亚伟，周雁舟，惠文涛 YAN Yawei, ZHOU Yanzhou, HUI Wentao 信息工程大学，郑州 450001 Information Engineering University, Zhengzhou 450001, China YAN Yawei, ZHOU Yanzhou, HUI Wentao. Research on application of model checking in integrity formal verifica- tion. Computer Engineering and Applications, 2017, 53 （4 ）：59-63. Abstract ：For the integration of information systems, the security of data is very important. Data integrity is one of the most important feature of data security. To ensure the security of information data increasing system reliability, it needs to be analyzed and verified for the integrity of data. To solve the quantitative assessment of data integrity, use probability calculations tree logic to describe formally definition of integrity and establishment Markov Decision Process evaluation model, then use probabilistic model check algorithm to evaluate integrity realizing quantitative verification of the integrity. Through applying the proposed evaluation model to interactive electronic manual system, quantitative calculate the integrity of the system model providing support for the integrity requirements of system development. Key words ：integrity; formally; probability; Probabilistic Computation Tree Logic（PCTL ）; model check 摘 要：对于信息系统而言，数据信息的安全性是十分重要的，数据的完整性是数据安全最重要的表现形式。为了 确保系统中数据信息的安全性，提高系统可靠性，需要对数据的完整性进行分析和验证。针对数据完整性的定量评 估问题，提出使用概率计算树逻辑对完整性定义进行形式化描述，并建立相应的马尔可夫决策过程定量评估模型， 运用概率模型检测算法对完整性进行的评估，实现对完整性的定量验证。通过把提出的评估模型应用于交互式电 子手册系统，定量计算出了该系统模型的完整性，为系统开发中的完整性需求提供支持。 关键词：完整性；形式化；概率分析；概率计算树逻辑；模型测试 文献标志码：A 中图分类号：TP311 doi ：10.3778/j.issn. 1002-8331.1507-0081 1 引言 性保护模型及其应用，对完整性定量评估的研究相对较 随着信息技术在各行各业的应用日益广泛，人们对 少。在完整性定义方面，Biba[1]把完整性定义为防止信 信息系统的依赖程度逐渐加强，对信息系统的安全性要 息从低完整性客体流向高完整性客体。Clark 和Wilson[2] 求也越来越高。数据信息同其他固定资产一样，对