模型检测在完整性形式化验证中的应用研究
来源：计算机工程与应用杂志2017年第4期北京时间：
作者：严亚伟，周雁舟，惠文涛
单位：信息工程大学，郑州 450001
摘要：对于信息系统而言，数据信息的安全性是十分重要的，数据的完整性是数据安全最重要的表现形式。为了确保系统中数据信息的安全性，提高系统可靠性，需要对数据的完整性进行分析和验证。针对数据完整性的定量评估问题，提出使用概率计算树逻辑对完整性定义进行形式化描述，并建立相应的马尔可夫决策过程定量评估模型，运用概率模型检测算法对完整性进行的评估，实现对完整性的定量验证。通过把提出的评估模型应用于交互式电子手册系统，定量计算出了该系统模型的完整性，为系统开发中的完整性需求提供支持。
关键词：完整性,形式化,概率分析,概率计算树逻辑,模型测试
