模型检测在完整性形式化验证中的应用研究  

Research on application of model checking in integrity formal verification

作　　者：严亚伟 周雁舟[1] 惠文涛[1] YAN Yawei;ZHOU Yanzhou;HUI Wentao(Information Engineering University, Zhengzhou 450001, China)

机构地区：[1]信息工程大学,郑州450001

出　　处：《计算机工程与应用》2017年第4期59-63,134,共6页Computer Engineering and Applications

摘　　要：对于信息系统而言,数据信息的安全性是十分重要的,数据的完整性是数据安全最重要的表现形式。为了确保系统中数据信息的安全性,提高系统可靠性,需要对数据的完整性进行分析和验证。针对数据完整性的定量评估问题,提出使用概率计算树逻辑对完整性定义进行形式化描述,并建立相应的马尔可夫决策过程定量评估模型,运用概率模型检测算法对完整性进行的评估,实现对完整性的定量验证。通过把提出的评估模型应用于交互式电子手册系统,定量计算出了该系统模型的完整性,为系统开发中的完整性需求提供支持。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.

关 键 词：完整性 形式化 概率分析 概率计算树逻辑 模型测试 

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