基于模型检测的策略冲突检测方法  

Policy Conflict Detection Method Based on Model Checking

作　　者：吴丹[1,2] 危胜军[2,3] 

机构地区：[1]北京理工大学机电学院,北京海淀区100081 [2]北京理工大学软件安全工程技术北京市重点实验室,北京海淀区100081 [3]北京理工大学软件学院,北京海淀区100081

出　　处：《电子科技大学学报》2013年第5期745-748,768,共5页Journal of University of Electronic Science and Technology of China

基　　金：国家863项目(2009AA01Z433)

摘　　要：提出一种基于模型校验的策略冲突检测新方法。首先通过形式化描述语言进行系统建模,采用时态逻辑表征策略冲突的系统属性,然后利用NuSMV模型检测器验证属性的可满足性,并根据模型检测器产生的反例轨迹追溯策略冲突点。该方法可提高策略冲突检测的效率。A new policy conflict detection method is proposed based on model checking. In this method, the model of system is specified with formal description language, the properties of system depending on different types of policy conflicts is represented with temporal logic, and the violations of properties is detected by using NuSMV model checker, which can provide the counterexample and trace it back to the policy conflict point. The result shows that the method can improve the efficiency of policy conflict detection.

关 键 词：反例 模型检测 NUSMV 策略冲突 

分 类 号：TP399[自动化与计算机技术—计算机应用技术]