責任政策形式化驗證方法

張濤,謝紅, 黃少濱

(1.哈爾濱工程大學 計算機科學與技術學院，黑龍江 哈爾濱 150001； 2.哈爾濱工程大學 信息與通信工程學院，黑龍江 哈爾濱 150001)

?

責任政策形式化驗證方法

張濤1，2,謝紅2, 黃少濱1

(1.哈爾濱工程大學 計算機科學與技術學院，黑龍江 哈爾濱 150001； 2.哈爾濱工程大學 信息與通信工程學院，黑龍江 哈爾濱 150001)

摘要：為了驗證多Agent系統(tǒng)設計的正確性，將責任政策作為約束多Agent交互行為的高層“需求規(guī)格”或“通信協(xié)議”，對其進行形式化建模及驗證。研究了建模責任政策的形式化框架語言，基于責任狀態(tài)模型建模責任政策的動態(tài)演化過程。給出了政策模型形式化驗證方法，將政策模型的操作語義定義為Kripke結構的狀態(tài)遷移系統(tǒng)，政策中Agent行為的約束規(guī)則聲明為線性時序邏輯公式，使用模型檢測器NuSMV驗證政策模型對線性時序邏輯公式的可滿足性。實驗結果表明，該方法可有效分析責任政策的設計缺陷，提高多Agent系統(tǒng)設計的正確性。

關鍵詞：多Agent系統(tǒng)； 形式化方法； 政策建模； 社會承諾； 模型檢測； 責任政策

網(wǎng)絡出版地址：http://www.cnki.net/kcms/detail/23.1390.u.20160308.1257.006.html

復雜適應系統(tǒng)中多Agent間的行為交互是系統(tǒng)具備“適應性”的前提，也是導致系統(tǒng)“復雜性”的主要原因之一[1]。為在系統(tǒng)設計過程中正確建模Agent間的交互行為，本文提出一種多Agent系統(tǒng)責任政策的形式化驗證方法。多Agent系統(tǒng)中，責任一般是Agent為了滿足某些要求而執(zhí)行的動作[2]，例如：“社會保障管理條例規(guī)定企業(yè)在成立之日起的20個工作日內(nèi)，需持營業(yè)執(zhí)照到當?shù)厣鐣ｋU經(jīng)辦機構辦理社會保險登記”。責任或是Agent被要求保持的某種狀態(tài)[3]，例如：“養(yǎng)老保險繳費人員必須處于參保狀態(tài)”。 由于責任政策約束其所屬領域內(nèi)Agent間的交互行為，可被視為系統(tǒng)設計中的高層 “需求規(guī)格”[4]或“通信協(xié)議”[5]，形式化驗證責任政策有助于明晰政策的描述和解釋，正確設計多Agent交互行為，提高系統(tǒng)的正確性和可靠性。1987年Minsky首次在計算機科學領域提出研究規(guī)律政策的觀點[6]，隨后發(fā)表了關于分布式系統(tǒng)中政策研究的開創(chuàng)性論文——規(guī)律控制的交互(law-governed interaction, LGI)[7]，由此激發(fā)了該領域的深遠研究與大量實踐工作。盡管LGI模型曾被成功用于多Agent系統(tǒng)的各種研究與應用領域，但該模型使用低層抽象信息描述系統(tǒng)中的交互行為，使其逐漸不能滿足復雜系統(tǒng)的設計需求，原因在于一旦政策規(guī)則由頂層概念映射為底層通信原語時就會丟失其原始語義。這種抽象遠離具體領域是所有此類語言共有的問題，為此多種責任政策的形式化語言和方法被相繼提出[8-11]，這些方法可大致被分為兩類：一類是設計政策執(zhí)行語言，如文獻[9]，這類語言可對政策進行簡單的描述和解釋，但由于缺乏形式語義所以不能對其進行形式分析或性質(zhì)驗證；另一類是設計政策分析語言，如文獻[8,11]，它們允許對政策進行形式化定義與分析，但是這類方法沒有定義政策語言執(zhí)行與管理的動態(tài)操作語義，不能作為自動驗證技術的形式化基礎。針對上述問題，本文提出一種責任政策形式化框架語言，將責任定義一種特殊的社會承諾，通過定義責任狀態(tài)模型建模責任政策的動態(tài)執(zhí)行過程，并為框架語言定義Kripke結構的操作語義，將其轉(zhuǎn)換為模型檢測器的輸入模型，自動執(zhí)行形式化驗證。

1社會承諾

社會承諾[12]是一種以公開化方法描述交互行為的約定，每一個承諾都由被稱為承諾方的Agent發(fā)起，并攜帶某些事實或行為序列指向被稱為承諾接收方的Agent。社會學方法使用承諾動作集合操作承諾，集合中的動作主要包括：創(chuàng)建、激活、撤銷、違反、釋放、授權、分配等[13]。由于基于社會承諾的研究方法僅關心承諾本身和承諾的執(zhí)行情況，而不必考慮Agent的內(nèi)部結構，其在建模業(yè)務過程[14]、開發(fā)人工制度[15]、驗證程序通信[16]、建模Agent交互[17]等研究領域得到了廣泛應用。社會承諾的形式化定義如下：

定義1社會承諾(social commitment,SC)。SC=(id,debtor,creditor,φ)是一個四元組，其中：id是社會承諾的標識，debtor是社會承諾發(fā)起方， creditor是社會承諾接收方，φ是聲明承諾內(nèi)容的公式。

社會承諾被創(chuàng)建后，debtor將向creditor傳遞由φ表示的事實或需要執(zhí)行的動作，例如：“企業(yè)向社會保險經(jīng)辦機構承諾申請辦理社會保險登記”可被表示為SC=(1,Ag1,Ag2,register(Ag1,Ag2)),其中Ag1表示企業(yè)，Ag2表示社會保險經(jīng)辦機構，謂詞公式register(Ag1,Ag2)表示Ag1向Ag2執(zhí)行“登記”活動。社會承諾包含以下幾種狀態(tài)：非活躍狀態(tài)inactive、活躍狀態(tài)active、違反狀態(tài)violated、履行狀態(tài)fulfilled。社會承諾通過承諾動作集合操作承諾改變承諾的狀態(tài)。

在多Agent系統(tǒng)中，政策中的責任可被認為是一種復雜的社會承諾，但是社會承諾的定義并不能完整表示責任政策的形式語義，如：責任政策環(huán)境、各種責任類型、責任狀態(tài)模型以及政策執(zhí)行需滿足的性質(zhì)要求等。下面本文擴展社會承諾的概念，定義責任以及責任政策語言。

2責任政策語言

責任政策描述了Agent被允許或禁止保持某種狀態(tài)或執(zhí)行某些活動，并關聯(lián)著一些條件集合，這些條件以環(huán)境的形式存在于責任描述中，描述系統(tǒng)狀態(tài)以及政策的應用規(guī)則。因此，在定義責任政策語言前，需先定義責任政策環(huán)境。與責任相關的環(huán)境主要有兩種，分別是基于狀態(tài)的環(huán)境和基于事件的環(huán)境。基于狀態(tài)的環(huán)境聲明政策中責任的狀態(tài)環(huán)境，基于事件的環(huán)境聲明責任被激活、失效、違反或履行的時刻?；跔顟B(tài)的責任環(huán)境表達式為：Cs(Ag1,Ag2,φ)←p1,p2,...,pn,其形式語義定義為當命題公式p1,p2,...,pn為真，Ag1向Ag2承諾φ時所在的環(huán)境Cs有效?？紤]如下示例：insuranced(Ag1,_,_)←participating(Ag1,endowment_insurance),assigned(Ag2,Ag1)，其聲明在Ag1參加養(yǎng)老保險，并被分配給相應管理機構Ag2的條件下，環(huán)境insuranced對于Ag1、任意客體、任意承諾有效，即環(huán)境insuranced聲明Ag1處于參保狀態(tài)?；谑录沫h(huán)境則描述了基于狀態(tài)的環(huán)境開始有效和終止有效的時刻，其被聲明為start(Cs)和end(Cs)。例如：當Agent參加養(yǎng)老保險時，基于事件的環(huán)境start(insuranced)為真，當Agent退出養(yǎng)老保險時，基于事件的環(huán)境end(insuranced)為真。責任政策的環(huán)境表達式聲明如下：

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

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

C::=Cs|Ce

其中，C表示責任政策的環(huán)境表達式；Cs是基于狀態(tài)的環(huán)境表達式；Ce是基于事件的環(huán)境表達式；c是用戶定義的基于狀態(tài)的環(huán)境標識符；[Cs1,Cs2]表示一個區(qū)間，其聲明基于狀態(tài)的環(huán)境在Cs1為真時開始有效，在Cs2為真時終止有效。

定義2責任(Obligation)。責任被定義為一種社會承諾Obligation=(N,debtor,creditor,φ,Ca,Cv)，其中，N是責任標識符，debtor是責任的發(fā)起方，creditor是責任的接收方，φ是聲明責任內(nèi)容的邏輯公式，Ca是責任的激活環(huán)境，Cv是責任的違反環(huán)境。下面在責任概念基礎上定義責任政策語言。

定義3責任政策語言(obligation policy language, OPL).OPL=(A,O,C,Action,R,sta)是一個六元組，其中：A是政策中所有Agent的集合，?Agi∈A,i∈N，Agi既可以是責任的debtor也可以是creditor；O是政策中所有責任的集合；C是政策環(huán)境的集合；Action=Acto∪Actc是政策動作的集合，Acto={create,active,fulfil,violate,deactivate}是責任操作動作的集合，Actc是責任內(nèi)容中動作的集合，即責任內(nèi)容中debtor承諾執(zhí)行的動作；R是責任政策執(zhí)行需滿足的時序性質(zhì)集合。sta:O→A是一個責任分配函數(shù)，給出每個責任所歸屬的Agent。

3責任政策語言的表達能力

責任政策語言OPL應具備清晰簡潔的語義，方便非專業(yè)人員理解和使用，該特點主要通過定義責任政策語言的責任類型、責任狀態(tài)模型實現(xiàn)。

3.1責任的類型

責任政策語言OPL所能表達的責任類型主要包括：持久型責任、非持久型責任以及連續(xù)型責任。

持久型責任是被激活后，在被debtor履行前不會失效的責任。持久型責任的激活環(huán)境Ca既可以是基于事件的環(huán)境表達式start(Cs)也可以是基于狀態(tài)的環(huán)境表達式[Cs,false]。因此，持久型政策的定義條件可被表示為end(Ca)=false。例如對于養(yǎng)老保險參保人繳納養(yǎng)老保險費的責任描述如下：Obligation=(n1,Ag1,Ag2,φ1,start(june),end(june))，其中，Ag1是養(yǎng)老保險參保人員，Ag2是養(yǎng)老保險管理機構，φ1=pay_fees(Ag1,Ag2)表示Ag1向Ag2繳納費款的行為。環(huán)境june的形式聲明為：june(Ag1，pay_fees,Ag2)←current_month(june)，其表示當前月是june時，環(huán)境june對Ag1和Ag2以及行為pay_fees有效。責任n1的激活環(huán)境是基于事件的環(huán)境表達式，其與基于的狀態(tài)環(huán)境表達式[start(june),false]等價。責任n1在激活后不會失效直至其被履行，如果責任在其違反環(huán)境end(june)為真時仍未被履行，則該責任被違反。

非持久型責任是被激活后可能發(fā)生失效的責任，其定義條件可表示為：end(Ca)≠false。例如考慮養(yǎng)老保險管理機構管理在職參保人員信息的責任：在職參保人在當?shù)貐⒓羽B(yǎng)老保險，則當?shù)氐酿B(yǎng)老保險管理機構負責管理該人員的個人信息直至管理期結束(即該參保人退休)，如果參保人轉(zhuǎn)移到異地參加養(yǎng)老保險，則原管理機構的管理責任就會發(fā)生失效。上述責任可被形式化的描述如下：Obligation=(n2,Ag2,Ag1,φ2,assigned_person,end(manage_time))，其中φ2=manage(Ag2,Ag1)聲明Ag2對Ag1的管理行為。責任的激活環(huán)境為：assigned_person(Ag2,_,Ag1)←assigned(Ag2,Ag1)，其聲明當Ag1被分配給Ag2管理時，環(huán)境assigned_person對于Ag2和Ag1以及任意行為有效。責任的違反環(huán)境被描述為manage_time(Ag2,_,_)←manage_start(Ag2,T1),manage_start(Ag2,T2),current_time(T),T1≤T≤T2，其中T1和T2分別是Ag2負責管理責任的起始時間與終止時間，當前時間T在[T1,T2]區(qū)間內(nèi)時，環(huán)境manage_time對Ag2、任意客體、任意行為有效。因此，當在職參保人Ag1分配給養(yǎng)老保險管理機構Ag2管理時，責任n2被激活。如果Ag2在其管理時間截止時沒有履行管理責任，則該責任被違反，如果Ag1不再由Ag2管理，則該責任失效。

連續(xù)型責任聲明系統(tǒng)中有維持事物狀態(tài)需求的責任，在系統(tǒng)中這種責任從環(huán)境起始直至環(huán)境結束都要求其保持激活狀態(tài)，例如考慮如下責任Obligation=(n3,Ag1,Ag2,φ3,insuranced,below_limit_payment)，責任n3聲明參加養(yǎng)老保險的職工Ag1向管理機構Ag2繳費不能低于繳費下限。其中Ag1是養(yǎng)老保險參保人員，Ag2是養(yǎng)老保險管理機構，φ3=pay_fees(Ag1,Ag2)聲明Ag1向Ag2執(zhí)行繳費行為，狀態(tài)環(huán)境低于費款下限below_limit_fees被定義為below_limit_payment(Ag1,_,_)←limit_payment(Ag1,x1),current_payment(Ag1,x2),x2x1，其聲明參保人員繳納保險費低于政策規(guī)定的繳費下限的情況。

3.2責任的狀態(tài)模型

本文通過定義責任的狀態(tài)模型描述責任政策的動態(tài)演化過程。責任的狀態(tài)模型聲明了debtor執(zhí)行責任操作動作導致責任狀態(tài)變化的情況。根據(jù)責任類型的語義，責任狀態(tài)模型被分為兩種：連續(xù)型責任狀態(tài)模型和非連續(xù)型責任狀態(tài)模型，分別如圖1和圖2所示。

圖1　連續(xù)型責任的狀態(tài)模型Fig.1　The state model of continuous obligation

圖2　非連續(xù)型責任的狀態(tài)模型Fig.2　The state model of discontinuous obligation

在責任狀態(tài)模型中，責任Obligation=(N,debtor,creditor,φ,Ca,Cv)的狀態(tài)主要包括：

初始狀態(tài)“?”，此狀態(tài)表示責任未被創(chuàng)建。

非活躍狀態(tài)inactive，其可被形式化聲明為inactive(obligation)→(create(debtor,obligation)∧(start(Ca))∨end(Ca)))。責任處于非活躍狀態(tài)主要有兩種可能：1)責任創(chuàng)建后未被要求履行，即create(debtor,obligation)∧start(Ca)；2)責任在創(chuàng)建后曾被激活過，但現(xiàn)已不在被要求履行，即環(huán)境end(Ca)有效，此時責任同樣處于非活躍狀態(tài)。

活躍狀態(tài)active，其可被形式化聲明為active(obligation)←active(debtor,obligation)∧start(Ca)。當責任被要求履行時，即環(huán)境start(Ca)有效，由debtor激活責任使其處于活躍狀態(tài)。

履行狀態(tài)fulfilled，其可被形式化聲明為fulfilled(obligation)←fulfil(debtor,obligation)∧start(Ca)。責任在激活環(huán)境下被debtor履行后，責任處于履行狀態(tài)。

違反狀態(tài)violated，其可被形式化聲明為violated(obligation)←violate(debtor,obligation)∧start(Ca)∧start(Cv)。責任在激活環(huán)境和違反環(huán)境有效的條件下被debtor違反，則其處于違反狀態(tài)。

違反/非活躍狀態(tài)violated/inactive， violated/inactive(obligation)←(violated(obligation)∧end(Ca)∧deactivate(debtor,obligation)。責任被debtor違反后，在激活環(huán)境終止有效的條件下，debtor執(zhí)行deactivate行為使責任處于違反/非活躍狀態(tài)。

違反/履行狀態(tài)violated/fulfilled，可被聲明為violated/fulfilled(obligation)←(violated(obligation)∧start(Ca)∧fulfil(debtor,obligation)。責任被違反后，且在激活環(huán)境有效的條件下被debtor履行，則責任處于違反/履行狀態(tài)。

責任狀態(tài)模型中的違反狀態(tài)被定義為持久狀態(tài)，即一旦責任的違反環(huán)境為真且debtor執(zhí)行違反操作，則責任處于違反狀態(tài)并在后續(xù)的狀態(tài)演化中保持違反狀態(tài)。

3.3責任執(zhí)行的規(guī)則

責任政策的執(zhí)行規(guī)則實質(zhì)上是Agent之間交互行為應滿足的各種時序性質(zhì)，本文使用線性時序邏輯(linear temporal logic, LTL)聲明責任政策的執(zhí)行規(guī)則。LTL公式由原子命題、邏輯連接符以及模態(tài)算子構成，其中邏輯連接符包括：、∧、∨、→，模態(tài)算子包括：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公式。

基于線性時序邏輯，責任政策執(zhí)行規(guī)則的集合R是描述政策行為安全性、活性等時序性質(zhì)的公式集合，例如：對于政策行為的活性性質(zhì)，參保人員履行參加保險的責任n1，則參保人最終總是能夠履行領取養(yǎng)老保險待遇的責任n5，其LTL公式描述為：G(fufilled(n1)→F(fulfilled(n5)))。

4模型檢測OPL

模型檢測(model checking)[18]是一種形式化驗證過程中面向有窮狀態(tài)并發(fā)系統(tǒng)的自動分析和驗證技術。為使用模型檢測技術驗證OPL所聲明的責任政策模型是否滿足規(guī)范，本文將OPL的形式語義定義為具有Kripke結構的狀態(tài)遷移系統(tǒng)，根據(jù)該形式語義將OPL模型轉(zhuǎn)換為模型檢測器NuSMV 的輸入模型，用NuSMV執(zhí)行自動驗證。

4.1OPL的形式語義

定義5遷移系統(tǒng)(transition system, TS)[18].遷移系統(tǒng)是一個六元組：TS=(S,Act,→,I,AP,L)，其中：1)S是系統(tǒng)狀態(tài)的有窮集合。Act是系統(tǒng)動作的有窮集合。→?S×Act×S表示狀態(tài)遷移關系集合。I?S是系統(tǒng)初始狀態(tài)的有窮集合。AP是原子命題的有窮集合。L:S→2AP是一個標簽函數(shù)。

定義6責任政策語言OPL的操作語義。OPL=(A,O,C,Action,R,sta)的操作語義是一個六元組：TSOPL=(S,Act,→,I,AP,L)，其中：S?(sta(o1)×...×sta(on))×C是系統(tǒng)狀態(tài)的有窮集合。Act=Action是動作的有窮集合?！?S×Act×S表示狀態(tài)遷移關系集合。I?(?1×...×?n)×C是系統(tǒng)初始狀態(tài)的有窮集合。AP是原子命題的有窮集合。L:S→2AP是標簽函數(shù)。

在狀態(tài)遷移系統(tǒng)TSOPL中，系統(tǒng)狀態(tài)集合S中的狀態(tài)由當前時刻每個責任所處狀態(tài)和責任政策的當前環(huán)境組成。系統(tǒng)初始狀態(tài)由每個責任的初始狀態(tài)和系統(tǒng)初始時刻的責任環(huán)境組成。TSOPL的動作集合Act與OPL的動作集合Action定義相同，即Act=Acto∪Actc，Acto是責任操作動作的集合，Actc是責任內(nèi)容中所執(zhí)行動作的集合。在OPL中，Actc中動作的發(fā)生導致責任政策環(huán)境發(fā)生變化，而Acto中動作的發(fā)生導致責任狀態(tài)發(fā)生變化，所以基于Act中的狀態(tài)、動作執(zhí)行序列可描述責任政策規(guī)則的執(zhí)行以及責任狀態(tài)的演變。AP集合中的元素是政策環(huán)境表達式與責任內(nèi)容公式φ中的原子命題。

4.2執(zhí)行NuSMV驗證

NuSMV是一種形式化驗證有限狀態(tài)并發(fā)系統(tǒng)的符號模型檢測器，驗證過程中并發(fā)系統(tǒng)被建模為的NuSMV輸入模型，與聲明系統(tǒng)性質(zhì)的時序邏輯公式一同輸入模型檢測其中執(zhí)行自動驗證。NuSMV輸入模型由一個或多個模塊組成，其中一個模塊必須被聲明為主模塊，每個模塊都可由三部分組成：變量的聲明、變量賦值以及性質(zhì)聲明。模塊內(nèi)部聲明變量并對變量賦值，賦值操作通常給出變量的初始值，而變量下一個值是關于變量當前值的表達式。NuSMV建模語言的具體語法可參照文獻[18]。

本文基于OPL模型的操作語義，將OPL模型轉(zhuǎn)換為NuSMV的輸入模型，與聲明政策執(zhí)行規(guī)則的LTL公式一同輸入到NuSMV中，自動驗證OPL模型對LTL公式的可滿足性。在轉(zhuǎn)換過程中，OPL模型中的Agent被轉(zhuǎn)換為獨立的模塊，并在主模塊中實例化，Agent所關聯(lián)責任的狀態(tài)以及模型的環(huán)境變量被定義為模塊中的變量，與狀態(tài)相關的責任操作動作被轉(zhuǎn)換為狀態(tài)演化的推理規(guī)則，基于狀態(tài)和責任操作動作的遷移關系定義在模塊ASSIGN部分，責任的內(nèi)部動作被轉(zhuǎn)換為遷移條件定義在模塊的next語句中。下面通過具體實例說明轉(zhuǎn)換責任政策OPL模型到NuSMV模型并執(zhí)行模型檢測的過程。

5責任政策模型檢測實例

以《城鎮(zhèn)企業(yè)職工基本養(yǎng)老保險關系轉(zhuǎn)移接續(xù)暫行辦法》為例，后文簡稱《暫行辦法》，首先創(chuàng)建該政策的OPL模型，并將其轉(zhuǎn)換為NuSMV輸入模型執(zhí)行模型檢測，最后基于模型檢測驗證結果分析暫行辦法背后的利益博弈關系。

《暫行辦法》于2009年頒布,其總體目標是“方便養(yǎng)老保險關系的轉(zhuǎn)移，切實保障參保人員的合法利益 ，促進人力資源合理配置”。其中的各項條款規(guī)定了基本養(yǎng)老保險參保人員繳納基本養(yǎng)老保險金、轉(zhuǎn)移基本養(yǎng)老關系以及享受基本養(yǎng)老保險待遇的條件和經(jīng)辦流程。限于篇幅，本文不對《暫行辦法》的內(nèi)容一一介紹，僅介紹與本文有關的一些重要內(nèi)容，具體如下：

1)第二條給出了《暫行辦法》的適用范圍，尤其強調(diào)包括農(nóng)民工。

2)第三條給出了跨省流動參保人員達到基本養(yǎng)老保險待遇領取條件和未達到待遇領取年齡前，基本養(yǎng)老保險關系和個人賬戶的具體處理辦法，特別強調(diào)了不得辦理退保手續(xù)。

3)第四條規(guī)定了如何計算轉(zhuǎn)移基金，增加了按照實際繳費工資的12%轉(zhuǎn)移統(tǒng)籌基金，更好地平衡地方利益。

4)第六條規(guī)定了參保人保險關系不在戶籍所在地，則累計繳費年限必須滿10年，才可在保險關系所在地享受基本養(yǎng)老保險待遇。

5)第七條規(guī)定了參保人員轉(zhuǎn)移接續(xù)后，符合待遇領取條件的按照國發(fā)2005年38號文的規(guī)定享受基本養(yǎng)老金，確保轉(zhuǎn)移人員的基本養(yǎng)老金計算辦法與其他參保人員的一致性。

6)第十一條要求各地轉(zhuǎn)移接續(xù)相關政策以《暫行辦法》規(guī)定為準。

《暫行辦法》在統(tǒng)一我國各地養(yǎng)老關系轉(zhuǎn)移的差異性，在保護農(nóng)民工參保權益、平衡地方利益、堵塞制度漏洞方面有著重要的意義，在基本養(yǎng)老保險政策仿真過程中可作為多Agent交互行為的建模依據(jù)。

對于《暫行辦法》OPL模型OPL=(A,O,C,Action,R,sta)， Agent集合A主要包括：社保經(jīng)辦機構PB、參保人GR、基本養(yǎng)老保險關系轉(zhuǎn)入地INTOPLACE、基本養(yǎng)老保險關系轉(zhuǎn)出地OUTPLACE。建模過程中，《暫行辦法》的各條規(guī)定被形式化為各Agent的具體責任和政策環(huán)境，構成OPL模型的責任集合O和環(huán)境集合C。限于篇幅，本文僅介紹與被驗證性質(zhì)相關的Agent及其責任。Agent GR的責任主要包括：參加保險n1，向管理機構登記n2，繳納保險費n3，申請參保關系轉(zhuǎn)移n4，領取保險待遇n5，退出保險n6。Agent PB的責任主要包括：同意轉(zhuǎn)移參保關系n7，支付保險待遇n8，同意退保n9。各責任的形式化定義如下：

Obligation=(n1,GR,PB,φ1,want_insured,over_age_limit)聲明50周歲以下的參保人GR可以參加城鎮(zhèn)基本養(yǎng)老保險，其中φ1=participating(GR,endowment_insurance)聲明參保人參加養(yǎng)老保險的行為，布爾型的環(huán)境want_insured聲明參保人是否要參保，環(huán)境over_age_limit←age(GR)>50聲明參保人年齡下限為50周歲。

Obligation=(n2,GR,PB,φ2insuranced,not_alive)聲明參保人GR在社保經(jīng)辦機構PB登記注冊，由PB管理GR，其中φ2=register(PB,GR)，環(huán)境insuranced(GR,_,_)←participating(GR,endowment_insurance)聲明GR處于參保狀態(tài)，簡寫為insuranced。布爾型的環(huán)境not_alive聲明GR已死亡。

Obligation=(n3,GR,PB,φ3,insuranced,retired)聲明未退休參保人GR在退休前向PB繳納養(yǎng)老金，其中φ3=pay_fees(GR,PB)，布爾型環(huán)境retired聲明GR是否處于退休狀態(tài)。

Obligation=(n4,GR,PB,φ4,insuranced∧want_transfer,retired)聲明未退休參保人GR向PB申請轉(zhuǎn)移參保關系，其中φ4=apply_transfer(GR,PB)，布爾型環(huán)境want_transfer聲明GR是否要轉(zhuǎn)移參保關系。

Obligation=(n5,GR,PB,φ5,insuranced∧retired∧acc_payment_year，not_alive)聲明活著的已退休參保人達到繳費年限可領取社保機構支付的基本養(yǎng)老保險待遇，其中φ5=get_money(GR,PB)，布爾型環(huán)境變量acc_payment_year聲明GR是否達到繳納養(yǎng)老保險的累計年限。

Obligation=(n6,GR,PB,φ6,insuranced∧retired，not_alive)聲明未退休參保人退出養(yǎng)老保險，φ6=apply_quit(GR,endowment_insurance)。

Obligation=(n7,PB,GR,φ7,insuranced∧want_transfer∧retired,not_alive)聲明PB同意未退休參保人GR轉(zhuǎn)移參保關系，其中φ7=agree_transfer(PB,GR)。

Obligation=(n8,PB,GR,φ8,insuranced∧retired∧achieve_payment_year,not_alive)聲明PB支付已退休參保人GR養(yǎng)老保險待遇，其中φ8=pay(PB,GR)，布爾型環(huán)境變量achieve_payment_year聲明參保人的累計繳費年限是否達到10年。

Obligation=(n9,PB,GR,φ9,insuranced∧achieve_payment_year,retired)聲明PB同意撤銷未退休但是已達到累計繳費年限的GR的參保關系，其中φ9=agree_quit(PB,GR)。

根據(jù)4.2節(jié)所述，在《暫行辦法》的OPL模型向SMV模型轉(zhuǎn)換過程中，Agent GR與Agent PB被建模為獨立的SMV模塊GR和PB，并在SMV主模塊main中實例化。在SMV主模塊中，政策的環(huán)境變量被初始化，政策應滿足的線性時序性質(zhì)被定義為LTL公式，《暫行辦法》的SMV模型如圖3所示。將圖3所示的模型輸入模型檢測器，驗證結果表明政策模型不滿足公式。

在實例分析中，被驗證的性質(zhì)公式為G((g.n1=fufilled)->F(g.n5=fufilled))，其含義為總是滿足如果參保人g履行參加保險的責任，則其最終一定會經(jīng)常履行獲得待遇支付的責任，該公式斷言如果參保人參保最終一定可以享受保險待遇。

分析驗證反例提供的錯誤運行跡，可發(fā)現(xiàn)產(chǎn)生驗證錯誤的主要原因在于: 由于《暫行辦法》第六條規(guī)定了參保人累計繳費年限必須滿10 a才可在當?shù)叵硎芑攫B(yǎng)老保險待遇。這就意味著，當前年齡在50歲以上的參保人，如果此前由于種種原因未能積累繳費年限，則已經(jīng)不可能享受基本養(yǎng)老保險待遇。同時《暫行辦法》第三條的規(guī)定又導致這些參保人員不能提前退保，因此這類參保人員將面臨著退休后既不能享受待遇又不能提前退保的尷尬境遇，此結果將為參保人帶來巨大的經(jīng)濟損失。

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

6結論

1)本文給出一種基于社會承諾和模型檢測技術的責任政策形式化驗證方法，可有效發(fā)現(xiàn)責任政策的設計缺陷，檢驗多Agent系統(tǒng)設計模型的正確性。

2)該方法的優(yōu)勢在于可簡單直接的建模責任政策，不需要引入過多的專家經(jīng)驗和人工參與，責任政策語言的Kripke結構化操作語義方便對其執(zhí)行形式化驗證，并且不妨礙語言的表達能力和簡單性。

在未來的研究工作中，基于OPL的形式化驗證可用于多種實際應用中，例如：建模安全需求[20]、服務系統(tǒng)監(jiān)控和形式化交互協(xié)議[21]、業(yè)務過程建模[22]等，并且將對OPL的建模能力向知識建模方向進行進一步擴展。

參考文獻：

[1]董孟高, 毛新軍, 常志明, 等. 自適應多Agent系統(tǒng)的運行機制和策略描述語言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)；中央高校基本科研業(yè)務費專項基金項目(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

網(wǎng)絡出版日期：2016-01-27.