责任政策形式化验证方法

张涛,谢红, 黄少滨

(1.哈尔滨工程大学 计算机科学与技术学院，黑龙江 哈尔滨 150001； 2.哈尔滨工程大学 信息与通信工程学院，黑龙江 哈尔滨 150001)



责任政策形式化验证方法

张涛1，2,谢红2, 黄少滨1

(1.哈尔滨工程大学 计算机科学与技术学院，黑龙江 哈尔滨 150001； 2.哈尔滨工程大学 信息与通信工程学院，黑龙江 哈尔滨 150001)

摘要：为了验证多Agent系统设计的正确性，将责任政策作为约束多Agent交互行为的高层“需求规格”或“通信协议”，对其进行形式化建模及验证。研究了建模责任政策的形式化框架语言，基于责任状态模型建模责任政策的动态演化过程。给出了政策模型形式化验证方法，将政策模型的操作语义定义为Kripke结构的状态迁移系统，政策中Agent行为的约束规则声明为线性时序逻辑公式，使用模型检测器NuSMV验证政策模型对线性时序逻辑公式的可满足性。实验结果表明，该方法可有效分析责任政策的设计缺陷，提高多Agent系统设计的正确性。

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

网络出版地址：http://www.cnki.net/kcms/detail/23.1390.u.20160308.1257.006.html

复杂适应系统中多Agent间的行为交互是系统具备“适应性”的前提，也是导致系统“复杂性”的主要原因之一[1]。为在系统设计过程中正确建模Agent间的交互行为，本文提出一种多Agent系统责任政策的形式化验证方法。多Agent系统中，责任一般是Agent为了满足某些要求而执行的动作[2]，例如：“社会保障管理条例规定企业在成立之日起的20个工作日内，需持营业执照到当地社会保险经办机构办理社会保险登记”。责任或是Agent被要求保持的某种状态[3]，例如：“养老保险缴费人员必须处于参保状态”。 由于责任政策约束其所属领域内Agent间的交互行为，可被视为系统设计中的高层 “需求规格”[4]或“通信协议”[5]，形式化验证责任政策有助于明晰政策的描述和解释，正确设计多Agent交互行为，提高系统的正确性和可靠性。1987年Minsky首次在计算机科学领域提出研究规律政策的观点[6]，随后发表了关于分布式系统中政策研究的开创性论文——规律控制的交互(law-governed interaction, LGI)[7]，由此激发了该领域的深远研究与大量实践工作。尽管LGI模型曾被成功用于多Agent系统的各种研究与应用领域，但该模型使用低层抽象信息描述系统中的交互行为，使其逐渐不能满足复杂系统的设计需求，原因在于一旦政策规则由顶层概念映射为底层通信原语时就会丢失其原始语义。这种抽象远离具体领域是所有此类语言共有的问题，为此多种责任政策的形式化语言和方法被相继提出[8-11]，这些方法可大致被分为两类：一类是设计政策执行语言，如文献[9]，这类语言可对政策进行简单的描述和解释，但由于缺乏形式语义所以不能对其进行形式分析或性质验证；另一类是设计政策分析语言，如文献[8,11]，它们允许对政策进行形式化定义与分析，但是这类方法没有定义政策语言执行与管理的动态操作语义，不能作为自动验证技术的形式化基础。针对上述问题，本文提出一种责任政策形式化框架语言，将责任定义一种特殊的社会承诺，通过定义责任状态模型建模责任政策的动态执行过程，并为框架语言定义Kripke结构的操作语义，将其转换为模型检测器的输入模型，自动执行形式化验证。

1社会承诺

社会承诺[12]是一种以公开化方法描述交互行为的约定，每一个承诺都由被称为承诺方的Agent发起，并携带某些事实或行为序列指向被称为承诺接收方的Agent。社会学方法使用承诺动作集合操作承诺，集合中的动作主要包括：创建、激活、撤销、违反、释放、授权、分配等[13]。由于基于社会承诺的研究方法仅关心承诺本身和承诺的执行情况，而不必考虑Agent的内部结构，其在建模业务过程[14]、开发人工制度[15]、验证程序通信[16]、建模Agent交互[17]等研究领域得到了广泛应用。社会承诺的形式化定义如下：

定义1社会承诺(social commitment,SC)。SC=(id,debtor,creditor,φ)是一个四元组，其中：id是社会承诺的标识，debtor是社会承诺发起方， creditor是社会承诺接收方，φ是声明承诺内容的公式。

社会承诺被创建后，debtor将向creditor传递由φ表示的事实或需要执行的动作，例如：“企业向社会保险经办机构承诺申请办理社会保险登记”可被表示为SC=(1,Ag1,Ag2,register(Ag1,Ag2)),其中Ag1表示企业，Ag2表示社会保险经办机构，谓词公式register(Ag1,Ag2)表示Ag1向Ag2执行“登记”活动。社会承诺包含以下几种状态：非活跃状态inactive、活跃状态active、违反状态violated、履行状态fulfilled。社会承诺通过承诺动作集合操作承诺改变承诺的状态。

在多Agent系统中，政策中的责任可被认为是一种复杂的社会承诺，但是社会承诺的定义并不能完整表示责任政策的形式语义，如：责任政策环境、各种责任类型、责任状态模型以及政策执行需满足的性质要求等。下面本文扩展社会承诺的概念，定义责任以及责任政策语言。

2责任政策语言

责任政策描述了Agent被允许或禁止保持某种状态或执行某些活动，并关联着一些条件集合，这些条件以环境的形式存在于责任描述中，描述系统状态以及政策的应用规则。因此，在定义责任政策语言前，需先定义责任政策环境。与责任相关的环境主要有两种，分别是基于状态的环境和基于事件的环境。基于状态的环境声明政策中责任的状态环境，基于事件的环境声明责任被激活、失效、违反或履行的时刻。基于状态的责任环境表达式为：Cs(Ag1,Ag2,φ)←p1,p2,...,pn,其形式语义定义为当命题公式p1,p2,...,pn为真，Ag1向Ag2承诺φ时所在的环境Cs有效。考虑如下示例：insuranced(Ag1,_,_)←participating(Ag1,endowment_insurance),assigned(Ag2,Ag1)，其声明在Ag1参加养老保险，并被分配给相应管理机构Ag2的条件下，环境insuranced对于Ag1、任意客体、任意承诺有效，即环境insuranced声明Ag1处于参保状态。基于事件的环境则描述了基于状态的环境开始有效和终止有效的时刻，其被声明为start(Cs)和end(Cs)。例如：当Agent参加养老保险时，基于事件的环境start(insuranced)为真，当Agent退出养老保险时，基于事件的环境end(insuranced)为真。责任政策的环境表达式声明如下：

Cs::=true|false|c|Cs∧Cs|Cs∨Cs|

Ce::=start(Cs)|end(Cs)|Cs∧Ce|Ce∧Cs

C::=Cs|Ce

其中，C表示责任政策的环境表达式；Cs是基于状态的环境表达式；Ce是基于事件的环境表达式；c是用户定义的基于状态的环境标识符；[Cs1,Cs2]表示一个区间，其声明基于状态的环境在Cs1为真时开始有效，在Cs2为真时终止有效。

定义2责任(Obligation)。责任被定义为一种社会承诺Obligation=(N,debtor,creditor,φ,Ca,Cv)，其中，N是责任标识符，debtor是责任的发起方，creditor是责任的接收方，φ是声明责任内容的逻辑公式，Ca是责任的激活环境，Cv是责任的违反环境。下面在责任概念基础上定义责任政策语言。

定义3责任政策语言(obligation policy language, OPL).OPL=(A,O,C,Action,R,sta)是一个六元组，其中：A是政策中所有Agent的集合，∀Agi∈A,i∈N，Agi既可以是责任的debtor也可以是creditor；O是政策中所有责任的集合；C是政策环境的集合；Action=Acto∪Actc是政策动作的集合，Acto={create,active,fulfil,violate,deactivate}是责任操作动作的集合，Actc是责任内容中动作的集合，即责任内容中debtor承诺执行的动作；R是责任政策执行需满足的时序性质集合。sta:O→A是一个责任分配函数，给出每个责任所归属的Agent。

3责任政策语言的表达能力

责任政策语言OPL应具备清晰简洁的语义，方便非专业人员理解和使用，该特点主要通过定义责任政策语言的责任类型、责任状态模型实现。

3.1责任的类型

责任政策语言OPL所能表达的责任类型主要包括：持久型责任、非持久型责任以及连续型责任。

持久型责任是被激活后，在被debtor履行前不会失效的责任。持久型责任的激活环境Ca既可以是基于事件的环境表达式start(Cs)也可以是基于状态的环境表达式[Cs,false]。因此，持久型政策的定义条件可被表示为end(Ca)=false。例如对于养老保险参保人缴纳养老保险费的责任描述如下：Obligation=(n1,Ag1,Ag2,φ1,start(june),end(june))，其中，Ag1是养老保险参保人员，Ag2是养老保险管理机构，φ1=pay_fees(Ag1,Ag2)表示Ag1向Ag2缴纳费款的行为。环境june的形式声明为：june(Ag1，pay_fees,Ag2)←current_month(june)，其表示当前月是june时，环境june对Ag1和Ag2以及行为pay_fees有效。责任n1的激活环境是基于事件的环境表达式，其与基于的状态环境表达式[start(june),false]等价。责任n1在激活后不会失效直至其被履行，如果责任在其违反环境end(june)为真时仍未被履行，则该责任被违反。

非持久型责任是被激活后可能发生失效的责任，其定义条件可表示为：end(Ca)≠false。例如考虑养老保险管理机构管理在职参保人员信息的责任：在职参保人在当地参加养老保险，则当地的养老保险管理机构负责管理该人员的个人信息直至管理期结束(即该参保人退休)，如果参保人转移到异地参加养老保险，则原管理机构的管理责任就会发生失效。上述责任可被形式化的描述如下：Obligation=(n2,Ag2,Ag1,φ2,assigned_person,end(manage_time))，其中φ2=manage(Ag2,Ag1)声明Ag2对Ag1的管理行为。责任的激活环境为：assigned_person(Ag2,_,Ag1)←assigned(Ag2,Ag1)，其声明当Ag1被分配给Ag2管理时，环境assigned_person对于Ag2和Ag1以及任意行为有效。责任的违反环境被描述为manage_time(Ag2,_,_)←manage_start(Ag2,T1),manage_start(Ag2,T2),current_time(T),T1≤T≤T2，其中T1和T2分别是Ag2负责管理责任的起始时间与终止时间，当前时间T在[T1,T2]区间内时，环境manage_time对Ag2、任意客体、任意行为有效。因此，当在职参保人Ag1分配给养老保险管理机构Ag2管理时，责任n2被激活。如果Ag2在其管理时间截止时没有履行管理责任，则该责任被违反，如果Ag1不再由Ag2管理，则该责任失效。

连续型责任声明系统中有维持事物状态需求的责任，在系统中这种责任从环境起始直至环境结束都要求其保持激活状态，例如考虑如下责任Obligation=(n3,Ag1,Ag2,φ3,insuranced,below_limit_payment)，责任n3声明参加养老保险的职工Ag1向管理机构Ag2缴费不能低于缴费下限。其中Ag1是养老保险参保人员，Ag2是养老保险管理机构，φ3=pay_fees(Ag1,Ag2)声明Ag1向Ag2执行缴费行为，状态环境低于费款下限below_limit_fees被定义为below_limit_payment(Ag1,_,_)←limit_payment(Ag1,x1),current_payment(Ag1,x2),x2x1，其声明参保人员缴纳保险费低于政策规定的缴费下限的情况。

3.2责任的状态模型

本文通过定义责任的状态模型描述责任政策的动态演化过程。责任的状态模型声明了debtor执行责任操作动作导致责任状态变化的情况。根据责任类型的语义，责任状态模型被分为两种：连续型责任状态模型和非连续型责任状态模型，分别如图1和图2所示。

图1　连续型责任的状态模型Fig.1　The state model of continuous obligation

图2　非连续型责任的状态模型Fig.2　The state model of discontinuous obligation

在责任状态模型中，责任Obligation=(N,debtor,creditor,φ,Ca,Cv)的状态主要包括：

初始状态“•”，此状态表示责任未被创建。

非活跃状态inactive，其可被形式化声明为inactive(obligation)→(create(debtor,obligation)∧(start(Ca))∨end(Ca)))。责任处于非活跃状态主要有两种可能：1)责任创建后未被要求履行，即create(debtor,obligation)∧start(Ca)；2)责任在创建后曾被激活过，但现已不在被要求履行，即环境end(Ca)有效，此时责任同样处于非活跃状态。

活跃状态active，其可被形式化声明为active(obligation)←active(debtor,obligation)∧start(Ca)。当责任被要求履行时，即环境start(Ca)有效，由debtor激活责任使其处于活跃状态。

履行状态fulfilled，其可被形式化声明为fulfilled(obligation)←fulfil(debtor,obligation)∧start(Ca)。责任在激活环境下被debtor履行后，责任处于履行状态。

违反状态violated，其可被形式化声明为violated(obligation)←violate(debtor,obligation)∧start(Ca)∧start(Cv)。责任在激活环境和违反环境有效的条件下被debtor违反，则其处于违反状态。

违反/非活跃状态violated/inactive， violated/inactive(obligation)←(violated(obligation)∧end(Ca)∧deactivate(debtor,obligation)。责任被debtor违反后，在激活环境终止有效的条件下，debtor执行deactivate行为使责任处于违反/非活跃状态。

违反/履行状态violated/fulfilled，可被声明为violated/fulfilled(obligation)←(violated(obligation)∧start(Ca)∧fulfil(debtor,obligation)。责任被违反后，且在激活环境有效的条件下被debtor履行，则责任处于违反/履行状态。

责任状态模型中的违反状态被定义为持久状态，即一旦责任的违反环境为真且debtor执行违反操作，则责任处于违反状态并在后续的状态演化中保持违反状态。

3.3责任执行的规则

责任政策的执行规则实质上是Agent之间交互行为应满足的各种时序性质，本文使用线性时序逻辑(linear temporal logic, LTL)声明责任政策的执行规则。LTL公式由原子命题、逻辑连接符以及模态算子构成，其中逻辑连接符包括：、∧、∨、→，模态算子包括：X(next)、F(eventually)、G(always)、U(until)和R(release)。LTL公式定义如下：

定义3LTL公式：

1)true和false 是LTL公式；

2)每个原子命题是LTL的(原子)公式；

4)如果φ、φ是公式，那么Gφ、Fφ、Xφ、φUφ和φRφ也是LTL公式。

基于线性时序逻辑，责任政策执行规则的集合R是描述政策行为安全性、活性等时序性质的公式集合，例如：对于政策行为的活性性质，参保人员履行参加保险的责任n1，则参保人最终总是能够履行领取养老保险待遇的责任n5，其LTL公式描述为：G(fufilled(n1)→F(fulfilled(n5)))。

4模型检测OPL

模型检测(model checking)[18]是一种形式化验证过程中面向有穷状态并发系统的自动分析和验证技术。为使用模型检测技术验证OPL所声明的责任政策模型是否满足规范，本文将OPL的形式语义定义为具有Kripke结构的状态迁移系统，根据该形式语义将OPL模型转换为模型检测器NuSMV 的输入模型，用NuSMV执行自动验证。

4.1OPL的形式语义

定义5迁移系统(transition system, TS)[18].迁移系统是一个六元组：TS=(S,Act,→,I,AP,L)，其中：1)S是系统状态的有穷集合。Act是系统动作的有穷集合。→⊆S×Act×S表示状态迁移关系集合。I⊆S是系统初始状态的有穷集合。AP是原子命题的有穷集合。L:S→2AP是一个标签函数。

定义6责任政策语言OPL的操作语义。OPL=(A,O,C,Action,R,sta)的操作语义是一个六元组：TSOPL=(S,Act,→,I,AP,L)，其中：S⊆(sta(o1)×...×sta(on))×C是系统状态的有穷集合。Act=Action是动作的有穷集合。→⊆S×Act×S表示状态迁移关系集合。I⊆(•1×...וn)×C是系统初始状态的有穷集合。AP是原子命题的有穷集合。L:S→2AP是标签函数。

在状态迁移系统TSOPL中，系统状态集合S中的状态由当前时刻每个责任所处状态和责任政策的当前环境组成。系统初始状态由每个责任的初始状态和系统初始时刻的责任环境组成。TSOPL的动作集合Act与OPL的动作集合Action定义相同，即Act=Acto∪Actc，Acto是责任操作动作的集合，Actc是责任内容中所执行动作的集合。在OPL中，Actc中动作的发生导致责任政策环境发生变化，而Acto中动作的发生导致责任状态发生变化，所以基于Act中的状态、动作执行序列可描述责任政策规则的执行以及责任状态的演变。AP集合中的元素是政策环境表达式与责任内容公式φ中的原子命题。

4.2执行NuSMV验证

NuSMV是一种形式化验证有限状态并发系统的符号模型检测器，验证过程中并发系统被建模为的NuSMV输入模型，与声明系统性质的时序逻辑公式一同输入模型检测其中执行自动验证。NuSMV输入模型由一个或多个模块组成，其中一个模块必须被声明为主模块，每个模块都可由三部分组成：变量的声明、变量赋值以及性质声明。模块内部声明变量并对变量赋值，赋值操作通常给出变量的初始值，而变量下一个值是关于变量当前值的表达式。NuSMV建模语言的具体语法可参照文献[18]。

本文基于OPL模型的操作语义，将OPL模型转换为NuSMV的输入模型，与声明政策执行规则的LTL公式一同输入到NuSMV中，自动验证OPL模型对LTL公式的可满足性。在转换过程中，OPL模型中的Agent被转换为独立的模块，并在主模块中实例化，Agent所关联责任的状态以及模型的环境变量被定义为模块中的变量，与状态相关的责任操作动作被转换为状态演化的推理规则，基于状态和责任操作动作的迁移关系定义在模块ASSIGN部分，责任的内部动作被转换为迁移条件定义在模块的next语句中。下面通过具体实例说明转换责任政策OPL模型到NuSMV模型并执行模型检测的过程。

5责任政策模型检测实例

以《城镇企业职工基本养老保险关系转移接续暂行办法》为例，后文简称《暂行办法》，首先创建该政策的OPL模型，并将其转换为NuSMV输入模型执行模型检测，最后基于模型检测验证结果分析暂行办法背后的利益博弈关系。

《暂行办法》于2009年颁布,其总体目标是“方便养老保险关系的转移，切实保障参保人员的合法利益 ，促进人力资源合理配置”。其中的各项条款规定了基本养老保险参保人员缴纳基本养老保险金、转移基本养老关系以及享受基本养老保险待遇的条件和经办流程。限于篇幅，本文不对《暂行办法》的内容一一介绍，仅介绍与本文有关的一些重要内容，具体如下：

1)第二条给出了《暂行办法》的适用范围，尤其强调包括农民工。

2)第三条给出了跨省流动参保人员达到基本养老保险待遇领取条件和未达到待遇领取年龄前，基本养老保险关系和个人账户的具体处理办法，特别强调了不得办理退保手续。

3)第四条规定了如何计算转移基金，增加了按照实际缴费工资的12%转移统筹基金，更好地平衡地方利益。

4)第六条规定了参保人保险关系不在户籍所在地，则累计缴费年限必须满10年，才可在保险关系所在地享受基本养老保险待遇。

5)第七条规定了参保人员转移接续后，符合待遇领取条件的按照国发2005年38号文的规定享受基本养老金，确保转移人员的基本养老金计算办法与其他参保人员的一致性。

6)第十一条要求各地转移接续相关政策以《暂行办法》规定为准。

《暂行办法》在统一我国各地养老关系转移的差异性，在保护农民工参保权益、平衡地方利益、堵塞制度漏洞方面有着重要的意义，在基本养老保险政策仿真过程中可作为多Agent交互行为的建模依据。

对于《暂行办法》OPL模型OPL=(A,O,C,Action,R,sta)， Agent集合A主要包括：社保经办机构PB、参保人GR、基本养老保险关系转入地INTOPLACE、基本养老保险关系转出地OUTPLACE。建模过程中，《暂行办法》的各条规定被形式化为各Agent的具体责任和政策环境，构成OPL模型的责任集合O和环境集合C。限于篇幅，本文仅介绍与被验证性质相关的Agent及其责任。Agent GR的责任主要包括：参加保险n1，向管理机构登记n2，缴纳保险费n3，申请参保关系转移n4，领取保险待遇n5，退出保险n6。Agent PB的责任主要包括：同意转移参保关系n7，支付保险待遇n8，同意退保n9。各责任的形式化定义如下：

Obligation=(n1,GR,PB,φ1,want_insured,over_age_limit)声明50周岁以下的参保人GR可以参加城镇基本养老保险，其中φ1=participating(GR,endowment_insurance)声明参保人参加养老保险的行为，布尔型的环境want_insured声明参保人是否要参保，环境over_age_limit←age(GR)>50声明参保人年龄下限为50周岁。

Obligation=(n2,GR,PB,φ2insuranced,not_alive)声明参保人GR在社保经办机构PB登记注册，由PB管理GR，其中φ2=register(PB,GR)，环境insuranced(GR,_,_)←participating(GR,endowment_insurance)声明GR处于参保状态，简写为insuranced。布尔型的环境not_alive声明GR已死亡。

Obligation=(n3,GR,PB,φ3,insuranced,retired)声明未退休参保人GR在退休前向PB缴纳养老金，其中φ3=pay_fees(GR,PB)，布尔型环境retired声明GR是否处于退休状态。

Obligation=(n4,GR,PB,φ4,insuranced∧want_transfer,retired)声明未退休参保人GR向PB申请转移参保关系，其中φ4=apply_transfer(GR,PB)，布尔型环境want_transfer声明GR是否要转移参保关系。

Obligation=(n5,GR,PB,φ5,insuranced∧retired∧acc_payment_year，not_alive)声明活着的已退休参保人达到缴费年限可领取社保机构支付的基本养老保险待遇，其中φ5=get_money(GR,PB)，布尔型环境变量acc_payment_year声明GR是否达到缴纳养老保险的累计年限。

Obligation=(n6,GR,PB,φ6,insuranced∧retired，not_alive)声明未退休参保人退出养老保险，φ6=apply_quit(GR,endowment_insurance)。

Obligation=(n7,PB,GR,φ7,insuranced∧want_transfer∧retired,not_alive)声明PB同意未退休参保人GR转移参保关系，其中φ7=agree_transfer(PB,GR)。

Obligation=(n8,PB,GR,φ8,insuranced∧retired∧achieve_payment_year,not_alive)声明PB支付已退休参保人GR养老保险待遇，其中φ8=pay(PB,GR)，布尔型环境变量achieve_payment_year声明参保人的累计缴费年限是否达到10年。

Obligation=(n9,PB,GR,φ9,insuranced∧achieve_payment_year,retired)声明PB同意撤销未退休但是已达到累计缴费年限的GR的参保关系，其中φ9=agree_quit(PB,GR)。

根据4.2节所述，在《暂行办法》的OPL模型向SMV模型转换过程中，Agent GR与Agent PB被建模为独立的SMV模块GR和PB，并在SMV主模块main中实例化。在SMV主模块中，政策的环境变量被初始化，政策应满足的线性时序性质被定义为LTL公式，《暂行办法》的SMV模型如图3所示。将图3所示的模型输入模型检测器，验证结果表明政策模型不满足公式。

在实例分析中，被验证的性质公式为G((g.n1=fufilled)->F(g.n5=fufilled))，其含义为总是满足如果参保人g履行参加保险的责任，则其最终一定会经常履行获得待遇支付的责任，该公式断言如果参保人参保最终一定可以享受保险待遇。

分析验证反例提供的错误运行迹，可发现产生验证错误的主要原因在于: 由于《暂行办法》第六条规定了参保人累计缴费年限必须满10 a才可在当地享受基本养老保险待遇。这就意味着，当前年龄在50岁以上的参保人，如果此前由于种种原因未能积累缴费年限，则已经不可能享受基本养老保险待遇。同时《暂行办法》第三条的规定又导致这些参保人员不能提前退保，因此这类参保人员将面临着退休后既不能享受待遇又不能提前退保的尴尬境遇，此结果将为参保人带来巨大的经济损失。

图3　政策的SMV模型Fig.3　The SMV model of policy

6结论

1)本文给出一种基于社会承诺和模型检测技术的责任政策形式化验证方法，可有效发现责任政策的设计缺陷，检验多Agent系统设计模型的正确性。

2)该方法的优势在于可简单直接的建模责任政策，不需要引入过多的专家经验和人工参与，责任政策语言的Kripke结构化操作语义方便对其执行形式化验证，并且不妨碍语言的表达能力和简单性。

在未来的研究工作中，基于OPL的形式化验证可用于多种实际应用中，例如：建模安全需求[20]、服务系统监控和形式化交互协议[21]、业务过程建模[22]等，并且将对OPL的建模能力向知识建模方向进行进一步扩展。

参考文献：

[1]董孟高, 毛新军, 常志明, 等. 自适应多Agent系统的运行机制和策略描述语言SADL[J]. 软件学报, 2011, 22(4): 609-624.

DONG Menggao, MAO Xinjun, CHANG Zhiming, et al. Running mechanism and strategy description language SADL for self-adaptive MAS[J]. Journal of software, 2011, 22(4): 609-624.

[2]MICHAEL L, PARKES D C, PFEFFER A. Specifying and monitoring economic environments using rights and obligations[J]. Autonomous agents and multi-agent systems, 2010, 20(2): 158-197.

[3]XU Dianxiang, SANFORD M, LIU Zhaoliang, et al. Testing access control and obligation policies[C]//International conference on computing, networking and communications. San Diego, USA, 2013: 540-544.

[5]BALDONI M, BAROGLIO C, MARENGO E, et al. Constitutive and regulative specifications of commitment protocols: a decoupled approach[J]. ACM transactions on intelligent systems and technology, 2013, 4(2): 1-25.

[6]MINSKY N H, ROZENSHTEIN D. A law-based approach to object-oriented programming[C]//Proceedings on object-oriented programming systems, languages and applications. New York, USA, 1987: 482-493.

[7]MINSKY N H, UNGUREANU V. Law-governed interaction: a coordination and control mechanism for heterogeneous distributed systems[J]. ACM transactions on software engineering methodology, 2000, 9(3): 273-305.

[8]CRAVEN R, LOBO J, MA Jiefei, et al. Expressive policy analysis with enhanced system dynamicity[C]//Proceedings of the 4th international symposium on information, computer, and Communications Security. New York, USA, 2009: 239-250.

[9]DOUGHERTY D J, FISLER K, KRISHNAMURTHI S. Obligations and their interaction with programs[C]//Proceedings of 12th European symposium on research in computer security. Dresden, Germany, 2007: 375-389.

[10]KATT B, ZHANG Xinwen, BREU R, et al. A general obligation model and continuity: enhanced policy enforcement engine for usage control[C]//Proceedings of the 13th ACM symposium on access control models and technologies. New York, USA, 2008: 123-132.

[11]EL RAKAIBY Y, CUPPENS F, CUPPENS-BOULAHIA N. Formalization and management of group obligations[C]//IEEE international symposium on policies for distributed systems and networks. London, England, 2009: 158-165.

[12]BENTAHAR J, EL-MENSHAWY M, QU Hongyang, et al. Communicative commitments: Model checking and complexity analysis[J]. Knowledge-based systems, 2012, 35: 21-34.

[13]CHESANI F, MELLO P, MONTALI M, et al. Representing and monitoring social commitments using the event calculus[J]. Autonomous agents and multi-agent systems, 2013, 27(1): 85-130.

[14]EL-MENSHAWY M, BENTAHAR J, DSSOULI R. Modeling and verifying business interactions via commitments and dialogue actions[C]//Proceedings of the 4th KES international symposium on agent and multi-agent systems. Gdynia, Poland, 2010: 11-21.

[15]FORNARA N, COLOMBETTI M. Specifying and enforcing norms in artificial institutions: A retrospective review[C]//Proceedings of the 9th international workshop on declarative agent languages and technologies. Taipei, Taiwan, 2012: 117-119.

[16]EL-MENSHAWY M, BENTAHAR J, EL KHOLY W, et al. Reducing model checking commitments for agent communication to model checking ARCTL and GCTL[J]. Autonomous agents and multi-agent systems, 2013, 27(3): 375-418.

[17]GÜNAY A, YOLUM P. Constraint satisfaction as a tool for modeling and checking feasibility of multiagent commitments[J]. Applied intelligence, 2013, 39(3): 489-509.

[18]BAIER C, KATOEN J P, LARSEN K G. Principles of model checking[M]. Cambridge: The MIT Press, 2008: 16-20.

[19]CLARKE E M, GRUMBERG O, PELED D A. Model checking[M]. Cambridge, MA: The MIT Press, 1999: 30-33.

[20]SCHNEIDER K, KNAUSS E, HOUMB S, et al. Enhancing security requirements engineering by organizational learning[J]. Requirements engineering, 2012, 17(1): 35-56.

[21]ROBINSON W N, PURAO S. Monitoring service systems from a language-action perspective[J]. IEEE transactions on services computing, 2011, 4(1): 17-30.

[22]GOVERNATORI G, ROTOLO A. A conceptually rich model of business process compliance[C]//Proceedings of the 7th Asia-Pacific conference on conceptual modelling. Brisbane, Australia, 2010: 3-12.

收稿日期：2015-01-07.

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

作者简介：张涛(1981-)，男，博士. 通信作者：张涛, E-mail: zhangtaohrbeu@163.com.

doi:10.11990/jheu.201501007

中图分类号：TP311.5

文献标志码：A

文章编号：1006-7043(2016)04-0585-07

Formal method for obligation policy

ZHANG Tao1,2, XIE Hong2, HUANG Shaobin1

(1.College of Computer Science and Technology, Harbin Engineering University, Harbin 150001, China; 2.College of Information and Communications Engineering, Harbin Engineering University, Harbin 150001, China)

Abstract：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 NuSMV 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.

Keywords：multiagent system; formal method; policy model; social commitment; model checking; obligation policy

网络出版日期：2016-01-27.