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

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