责任政策形式化验证方法  

Formal method for obligation policy

作　　者：张涛[1,2] 谢红[2] 黄少滨[1] 

机构地区：[1]哈尔滨工程大学计算机科学与技术学院,黑龙江哈尔滨150001 [2]哈尔滨工程大学信息与通信工程学院,黑龙江哈尔滨150001

出　　处：《哈尔滨工程大学学报》2016年第4期585-591,共7页Journal of Harbin Engineering University

基　　金：国家科技支撑计划(2012BAH08B02);中央高校基本科研业务费专项基金项目(HEUCF100603;HEUCF041204);黑龙江省博士后基金资助项目(3236310148)

摘　　要：为了验证多Agent系统设计的正确性,将责任政策作为约束多Agent交互行为的高层"需求规格"或"通信协议",对其进行形式化建模及验证。研究了建模责任政策的形式化框架语言,基于责任状态模型建模责任政策的动态演化过程。给出了政策模型形式化验证方法,将政策模型的操作语义定义为Kripke结构的状态迁移系统,政策中Agent行为的约束规则声明为线性时序逻辑公式,使用模型检测器Nu SMV验证政策模型对线性时序逻辑公式的可满足性。实验结果表明,该方法可有效分析责任政策的设计缺陷,提高多Agent系统设计的正确性。To verify the correctness of the multiagent system,in this study,we considered obligation policy as a high-level ＂requirements specification＂or ＂communication protocol＂for constraining agent interaction. We introduce a formal framework language for modeling obligation policy,model the dynamic execution of the obligation policy based on a state model,and develop a formal method for verifying the policy model. We define the operational semantics of the policy model as a state transition system,which has a Kripke structure. We also define the policy rules that constrain the agent behavior as linear time-sequence logic（ LTL） formulas. Finally,we use the model checker Nu SMV to verify whether the policy model satisfies the LTL formulas. The experimental results show that this method can effectively analyze the design flaws of the policy model and can improve the correctness of the design of the multiagent system.

关 键 词：多AGENT系统 形式化方法 政策建模 社会承诺 模型检测 责任政策 

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