張濤,謝紅, 黃少濱

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

?

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

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

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

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

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

1社會(huì)承諾

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

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

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

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

2責(zé)任政策語言

責(zé)任政策描述了Agent被允許或禁止保持某種狀態(tài)或執(zhí)行某些活動(dòng)，并關(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)境?；跔顟B(tài)的環(huán)境聲明政策中責(zé)任的狀態(tài)環(huán)境，基于事件的環(huán)境聲明責(zé)任被激活、失效、違反或履行的時(shí)刻?；跔顟B(tài)的責(zé)任環(huán)境表達(dá)式為：Cs(Ag1,Ag2,φ)←p1,p2,...,pn,其形式語義定義為當(dāng)命題公式p1,p2,...,pn為真，Ag1向Ag2承諾φ時(shí)所在的環(huán)境Cs有效。考慮如下示例：insuranced(Ag1,_,_)←participating(Ag1,endowment_insurance),assigned(Ag2,Ag1)，其聲明在Ag1參加養(yǎng)老保險(xiǎn)，并被分配給相應(yīng)管理機(jī)構(gòu)Ag2的條件下，環(huán)境insuranced對于Ag1、任意客體、任意承諾有效，即環(huán)境insuranced聲明Ag1處于參保狀態(tài)?；谑录沫h(huán)境則描述了基于狀態(tài)的環(huán)境開始有效和終止有效的時(shí)刻，其被聲明為start(Cs)和end(Cs)。例如：當(dāng)Agent參加養(yǎng)老保險(xiǎn)時(shí)，基于事件的環(huán)境start(insuranced)為真，當(dāng)Agent退出養(yǎng)老保險(xiǎn)時(shí)，基于事件的環(huán)境end(insuranced)為真。責(zé)任政策的環(huán)境表達(dá)式聲明如下：

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

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

C::=Cs|Ce

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

定義2責(zé)任(Obligation)。責(zé)任被定義為一種社會(huì)承諾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)是一個(gè)六元組，其中：A是政策中所有Agent的集合，?Agi∈A,i∈N，Agi既可以是責(zé)任的debtor也可以是creditor；O是政策中所有責(zé)任的集合；C是政策環(huán)境的集合；Action=Acto∪Actc是政策動(dòng)作的集合，Acto={create,active,fulfil,violate,deactivate}是責(zé)任操作動(dòng)作的集合，Actc是責(zé)任內(nèi)容中動(dòng)作的集合，即責(zé)任內(nèi)容中debtor承諾執(zhí)行的動(dòng)作；R是責(zé)任政策執(zhí)行需滿足的時(shí)序性質(zhì)集合。sta:O→A是一個(gè)責(zé)任分配函數(shù)，給出每個(gè)責(zé)任所歸屬的Agent。

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

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

3.1責(zé)任的類型

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

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

非持久型責(zé)任是被激活后可能發(fā)生失效的責(zé)任，其定義條件可表示為：end(Ca)≠false。例如考慮養(yǎng)老保險(xiǎn)管理機(jī)構(gòu)管理在職參保人員信息的責(zé)任：在職參保人在當(dāng)?shù)貐⒓羽B(yǎng)老保險(xiǎn)，則當(dāng)?shù)氐酿B(yǎng)老保險(xiǎn)管理機(jī)構(gòu)負(fù)責(zé)管理該人員的個(gè)人信息直至管理期結(jié)束(即該參保人退休)，如果參保人轉(zhuǎn)移到異地參加養(yǎng)老保險(xiǎn)，則原管理機(jī)構(gòu)的管理責(zé)任就會(huì)發(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管理時(shí)，環(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負(fù)責(zé)管理責(zé)任的起始時(shí)間與終止時(shí)間，當(dāng)前時(shí)間T在[T1,T2]區(qū)間內(nèi)時(shí)，環(huán)境manage_time對Ag2、任意客體、任意行為有效。因此，當(dāng)在職參保人Ag1分配給養(yǎng)老保險(xiǎn)管理機(jī)構(gòu)Ag2管理時(shí)，責(zé)任n2被激活。如果Ag2在其管理時(shí)間截止時(shí)沒有履行管理責(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)老保險(xiǎn)的職工Ag1向管理機(jī)構(gòu)Ag2繳費(fèi)不能低于繳費(fèi)下限。其中Ag1是養(yǎng)老保險(xiǎn)參保人員，Ag2是養(yǎng)老保險(xiǎn)管理機(jī)構(gòu)，φ3=pay_fees(Ag1,Ag2)聲明Ag1向Ag2執(zhí)行繳費(fèi)行為，狀態(tài)環(huán)境低于費(fèi)款下限below_limit_fees被定義為below_limit_payment(Ag1,_,_)←limit_payment(Ag1,x1),current_payment(Ag1,x2),x2x1，其聲明參保人員繳納保險(xiǎn)費(fèi)低于政策規(guī)定的繳費(fèi)下限的情況。

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

本文通過定義責(zé)任的狀態(tài)模型描述責(zé)任政策的動(dòng)態(tài)演化過程。責(zé)任的狀態(tài)模型聲明了debtor執(zhí)行責(zé)任操作動(dòng)作導(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)有效，此時(shí)責(zé)任同樣處于非活躍狀態(tài)。

活躍狀態(tài)active，其可被形式化聲明為active(obligation)←active(debtor,obligation)∧start(Ca)。當(dāng)責(zé)任被要求履行時(shí)，即環(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ī)則實(shí)質(zhì)上是Agent之間交互行為應(yīng)滿足的各種時(shí)序性質(zhì)，本文使用線性時(shí)序邏輯(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)每個(gè)原子命題是LTL的(原子)公式；

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

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

4模型檢測OPL

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

4.1OPL的形式語義

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

定義6責(zé)任政策語言O(shè)PL的操作語義。OPL=(A,O,C,Action,R,sta)的操作語義是一個(gè)六元組：TSOPL=(S,Act,→,I,AP,L)，其中：S?(sta(o1)×...×sta(on))×C是系統(tǒng)狀態(tài)的有窮集合。Act=Action是動(dòng)作的有窮集合?！?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)前時(shí)刻每個(gè)責(zé)任所處狀態(tài)和責(zé)任政策的當(dāng)前環(huán)境組成。系統(tǒng)初始狀態(tài)由每個(gè)責(zé)任的初始狀態(tài)和系統(tǒng)初始時(shí)刻的責(zé)任環(huán)境組成。TSOPL的動(dòng)作集合Act與OPL的動(dòng)作集合Action定義相同，即Act=Acto∪Actc，Acto是責(zé)任操作動(dòng)作的集合，Actc是責(zé)任內(nèi)容中所執(zhí)行動(dòng)作的集合。在OPL中，Actc中動(dòng)作的發(fā)生導(dǎo)致責(zé)任政策環(huán)境發(fā)生變化，而Acto中動(dòng)作的發(fā)生導(dǎo)致責(zé)任狀態(tài)發(fā)生變化，所以基于Act中的狀態(tài)、動(dòng)作執(zhí)行序列可描述責(zé)任政策規(guī)則的執(zhí)行以及責(zé)任狀態(tài)的演變。AP集合中的元素是政策環(huán)境表達(dá)式與責(zé)任內(nèi)容公式φ中的原子命題。

4.2執(zhí)行NuSMV驗(yàn)證

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Obligation=(n2,GR,PB,φ2insuranced,not_alive)聲明參保人GR在社保經(jīng)辦機(jī)構(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)聲明活著的已退休參保人達(dá)到繳費(fèi)年限可領(lǐng)取社保機(jī)構(gòu)支付的基本養(yǎng)老保險(xiǎn)待遇，其中φ5=get_money(GR,PB)，布爾型環(huán)境變量acc_payment_year聲明GR是否達(dá)到繳納養(yǎng)老保險(xiǎn)的累計(jì)年限。

Obligation=(n6,GR,PB,φ6,insuranced∧retired，not_alive)聲明未退休參保人退出養(yǎng)老保險(xiǎn)，φ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)老保險(xiǎn)待遇，其中φ8=pay(PB,GR)，布爾型環(huán)境變量achieve_payment_year聲明參保人的累計(jì)繳費(fèi)年限是否達(dá)到10年。

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

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

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

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

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

6結(jié)論

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

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

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

參考文獻(xiàn)：

[1]董孟高, 毛新軍, 常志明, 等. 自適應(yīng)多Agent系統(tǒng)的運(yùn)行機(jī)制和策略描述語言SADL[J]. 軟件學(xué)報(bào), 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.

基金項(xiàng)目：國家科技支撐計(jì)劃(2012BAH08B02)；中央高校基本科研業(yè)務(wù)費(fèi)專項(xiàng)基金項(xiàng)目(HEUCF100603, HEUCF041204) ；黑龍江省博士后基金資助項(xiàng)目(3236310148).

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

doi:10.11990/jheu.201501007

中圖分類號：TP311.5

文獻(xiàn)標(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.