張濤,謝紅, 黃少濱

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

?

責(zé)任政策形式化驗證方法

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

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

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

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

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

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

1社會承諾

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

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

社會承諾被創(chuàng)建后，debtor將向creditor傳遞由φ表示的事實或需要執(zhí)行的動作，例如：“企業(yè)向社會保險經(jīng)辦機構(gòu)承諾申請辦理社會保險登記”可被表示為SC=(1,Ag1,Ag2,register(Ag1,Ag2)),其中Ag1表示企業(yè)，Ag2表示社會保險經(jīng)辦機構(gòu)，謂詞公式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)中，政策中的責(zé)任可被認為是一種復(fù)雜的社會承諾，但是社會承諾的定義并不能完整表示責(zé)任政策的形式語義，如：責(zé)任政策環(huán)境、各種責(zé)任類型、責(zé)任狀態(tài)模型以及政策執(zhí)行需滿足的性質(zhì)要求等。下面本文擴展社會承諾的概念，定義責(zé)任以及責(zé)任政策語言。

2責(zé)任政策語言

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

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

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

C::=Cs|Ce

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

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

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

3責(zé)任政策語言的表達能力

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

3.1責(zé)任的類型

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

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

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

連續(xù)型責(zé)任聲明系統(tǒng)中有維持事物狀態(tài)需求的責(zé)任，在系統(tǒng)中這種責(zé)任從環(huán)境起始直至環(huán)境結(jié)束都要求其保持激活狀態(tài)，例如考慮如下責(zé)任Obligation=(n3,Ag1,Ag2,φ3,insuranced,below_limit_payment)，責(zé)任n3聲明參加養(yǎng)老保險的職工Ag1向管理機構(gòu)Ag2繳費不能低于繳費下限。其中Ag1是養(yǎng)老保險參保人員，Ag2是養(yǎng)老保險管理機構(gòu)，φ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責(zé)任的狀態(tài)模型

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

4模型檢測OPL

模型檢測(model checking)[18]是一種形式化驗證過程中面向有窮狀態(tài)并發(fā)系統(tǒng)的自動分析和驗證技術(shù)。為使用模型檢測技術(shù)驗證OPL所聲明的責(zé)任政策模型是否滿足規(guī)范，本文將OPL的形式語義定義為具有Kripke結(jié)構(gòu)的狀態(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)遷移關(guān)系集合。I?S是系統(tǒng)初始狀態(tài)的有窮集合。AP是原子命題的有窮集合。L:S→2AP是一個標(biāo)簽函數(shù)。

定義6責(zé)任政策語言O(shè)PL的操作語義。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)遷移關(guān)系集合。I?(?1×...×?n)×C是系統(tǒng)初始狀態(tài)的有窮集合。AP是原子命題的有窮集合。L:S→2AP是標(biāo)簽函數(shù)。

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

4.2執(zhí)行NuSMV驗證

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

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

5責(zé)任政策模型檢測實例

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

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

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

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

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

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

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

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

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

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

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)辦機構(gòu)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)移參保關(guān)系，其中φ4=apply_transfer(GR,PB)，布爾型環(huán)境want_transfer聲明GR是否要轉(zhuǎn)移參保關(guān)系。

Obligation=(n5,GR,PB,φ5,insuranced∧retired∧acc_payment_year，not_alive)聲明活著的已退休參保人達到繳費年限可領(lǐng)取社保機構(gòu)支付的基本養(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)移參保關(guā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的參保關(guān)系，其中φ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)境變量被初始化，政策應(yīng)滿足的線性時序性質(zhì)被定義為LTL公式，《暫行辦法》的SMV模型如圖3所示。將圖3所示的模型輸入模型檢測器，驗證結(jié)果表明政策模型不滿足公式。

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

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

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

6結(jié)論

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

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

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

參考文獻：

[1]董孟高, 毛新軍, 常志明, 等. 自適應(yīng)多Agent系統(tǒng)的運行機制和策略描述語言SADL[J]. 軟件學(xué)報, 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)；中央高?；究蒲袠I(yè)務(wù)費專項基金項目(HEUCF100603, HEUCF041204) ；黑龍江省博士后基金資助項目(3236310148).

作者簡介：張濤(1981-)，男，博士. 通信作者：張濤, E-mail: zhangtaohrbeu@163.com.

doi:10.11990/jheu.201501007

中圖分類號：TP311.5

文獻標(biāo)志碼：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)絡(luò)出版日期：2016-01-27.