穆勇安 劉瑋 高勝 葉幸瑜 王紫昊

摘 要：多agent自適應(yīng)系統(tǒng)在運(yùn)行過程中需要根據(jù)環(huán)境進(jìn)行自適應(yīng)調(diào)整。異構(gòu)agent能夠提高agent的使用效率和降低系統(tǒng)的構(gòu)建成本，但存在復(fù)雜的協(xié)作問題，因此提出一種基于概率時(shí)間自動(dòng)機(jī)的異構(gòu)多agent自適應(yīng)系統(tǒng)運(yùn)行時(shí)驗(yàn)證方法。該方法通過形式化描述異構(gòu)agent的功能特征并融合環(huán)境中的隨機(jī)因素構(gòu)建概率時(shí)間自動(dòng)機(jī)模型模擬自適應(yīng)系統(tǒng)的運(yùn)行過程，針對(duì)異構(gòu)agent之間的協(xié)作邏輯制定安全約束條件以確保系統(tǒng)運(yùn)行中狀態(tài)遷移流程的安全性。通過模型檢查結(jié)合運(yùn)行時(shí)定量驗(yàn)證方法進(jìn)行實(shí)驗(yàn)驗(yàn)證，在智能泊車系統(tǒng)案例中應(yīng)用該方法。實(shí)驗(yàn)結(jié)果表明，agent之間協(xié)作邏輯的正確性可以有效保證系統(tǒng)運(yùn)行時(shí)的穩(wěn)定性，且相較于不使用運(yùn)行時(shí)定量驗(yàn)證的初始系統(tǒng)在相同時(shí)間內(nèi)正常運(yùn)行的時(shí)間提升了21%左右。

關(guān)鍵詞：自適應(yīng)系統(tǒng)； 異構(gòu)agent； 概率時(shí)間自動(dòng)機(jī)； agent協(xié)作； 運(yùn)行時(shí)定量驗(yàn)證

中圖分類號(hào)：TP311.5?? 文獻(xiàn)標(biāo)志碼：A?? 文章編號(hào)：1001-3695（2023）12-032-3728-08

doi：10.19734/j.issn.1001-3695.2023.04.0158

Runtime verification of heterogeneous multiagent selfadaptive based on probabilistic timed automata

Abstract：The multiagent selfadaptive system requires adaptive adjustments based on the dynamic environment during its runtime. Heterogeneous agents can enhance the efficiency of agent utilization and reduce system construction costs， but also present complex collaboration issues. Therefore， this paper proposed a runtime verification method for heterogeneous multiagent selfadaptive systems based on probabilistic timed automata. The approach constructed a probabilistic timed automaton model by formally describing the functional characteristics of heterogeneous agents and integrating random factors in the environment to simulate the operation process of the selfadaptive system. Regarding the collaboration logic among heterogeneous agents， it established security constraints to ensure the security of state transition processes during system operation. It combined model checking with runtime quantitative verification methods to conduct experiment and applied it in the case of an intelligent unmanned parking system. Experimental results show that the correctness of the cooperation logic between agents can effectively ensure the stability of the system at runtime， and compared with the initial system without runtime quantitative verification， the uptime of the system is increased by about 21% at the same time.

Key words：selfadaptive system（SAS）; heterogeneous agent; probabilistic timed automata; agent cooperative; runtime quantitative verification

0 引言

自適應(yīng)系統(tǒng)（SAS）可以監(jiān)控環(huán)境及其自身的變化，通過規(guī)范和修改自身行為或結(jié)構(gòu)，以達(dá)到持續(xù)性地滿足用戶需求的目的[1]。將自適應(yīng)系統(tǒng)中的功能實(shí)體抽象和封裝為多agent，能有效提高自適應(yīng)系統(tǒng)的自適應(yīng)能力[2]。自適應(yīng)能力是指agent根據(jù)收集到的環(huán)境數(shù)據(jù)自主作出系統(tǒng)決策的能力，自適應(yīng)能力的高低是影響agent能否根據(jù)環(huán)境條件變化作出正確決策的關(guān)鍵因素。決策的正確與否會(huì)對(duì)SAS的運(yùn)行過程產(chǎn)生重大影響。例如，SAS的不正當(dāng)決策使系統(tǒng)狀態(tài)遷移錯(cuò)誤，則會(huì)導(dǎo)致系統(tǒng)運(yùn)行死鎖等重大后果。因此，在復(fù)雜環(huán)境下的自適應(yīng)驗(yàn)證問題已成為開發(fā)可靠的SAS[3]亟待解決的問題之一。

為了提高SAS決策的可靠性，最初采用系統(tǒng)測(cè)試的方法[4，5]。該方法通過各項(xiàng)測(cè)試設(shè)備與接口來判定SAS的功能是否合格，但這類測(cè)試方法無法預(yù)測(cè)和枚舉動(dòng)態(tài)環(huán)境下SAS運(yùn)行時(shí)可能產(chǎn)生的多種系統(tǒng)行為，無法反映系統(tǒng)在動(dòng)態(tài)環(huán)境下的運(yùn)行情況。Weyns在SAS的形式化描述方法上進(jìn)行了研究調(diào)查[6]，并指出形式化描述方法能夠準(zhǔn)確指定和驗(yàn)證SAS可能產(chǎn)生的多種行為，以提供SAS所需的服務(wù)質(zhì)量保證（quality of service，QoS）[7～10]。模型檢查技術(shù)是形式化描述方法的具體應(yīng)用，是將SAS形式化描述為可驗(yàn)證的系統(tǒng)模型，并驗(yàn)證其各項(xiàng)屬性是否滿足給定的公式規(guī)范[11]，但系統(tǒng)模型的狀態(tài)數(shù)量會(huì)影響驗(yàn)證過程，只能應(yīng)用于有限狀態(tài)的小型系統(tǒng)。為了使模型檢查技術(shù)能夠應(yīng)用到更復(fù)雜的大型SAS中，在模型檢查的基礎(chǔ)上引入數(shù)學(xué)分析和邏輯形式主義的形式化規(guī)范方法以輔助解決大規(guī)模復(fù)雜或無限狀態(tài)系統(tǒng)的驗(yàn)證問題[12，13]。該方法通過符號(hào)表達(dá)式等價(jià)驗(yàn)證的方法減少模型的路徑重復(fù)和狀態(tài)數(shù)量以降低對(duì)驗(yàn)證效率的影響。文獻(xiàn)[14]提出了一個(gè)在無界多agent系統(tǒng)中驗(yàn)證系統(tǒng)行為的框架，并給出了基于反抽象技術(shù)構(gòu)建抽象模型的驗(yàn)證方法，但該方法建立在agent所處環(huán)境狀態(tài)不會(huì)出現(xiàn)變化的情況下，無法驗(yàn)證在不確定性環(huán)境下系統(tǒng)agent的自適應(yīng)需求規(guī)劃。劉瑋等人[15]通過概率規(guī)劃來定量刻畫agent行為在隨機(jī)環(huán)境下的不確定性并關(guān)聯(lián)上下文狀態(tài)以獲得最優(yōu)的自適應(yīng)需求規(guī)劃。文獻(xiàn)[16～18]就SAS的安全性、可達(dá)性和穩(wěn)定性的驗(yàn)證問題進(jìn)行了研究，為SAS的驗(yàn)證提供了更多角度。

然而，上述方法通常應(yīng)用于SAS設(shè)計(jì)或維護(hù)等離線階段，無法處理在實(shí)際運(yùn)行過程中出現(xiàn)的不確定因素。如果SAS在運(yùn)行過程中出現(xiàn)需求和硬件設(shè)備故障等重大變化，可能會(huì)導(dǎo)致SAS的QoS下降，嚴(yán)重時(shí)甚至造成系統(tǒng)功能不可用的情況。因此，SAS的驗(yàn)證要適應(yīng)環(huán)境、需求的動(dòng)態(tài)變化以保障SAS運(yùn)行時(shí)的安全穩(wěn)定。

在運(yùn)行時(shí)使用形式化方法驅(qū)動(dòng)SAS的驗(yàn)證可以作為解決上述問題的可行方案[19]。運(yùn)行時(shí)、量化的驗(yàn)證技術(shù)是基于形式化驅(qū)動(dòng)SAS重構(gòu)的一種數(shù)學(xué)方法。該方法通過構(gòu)建SAS及其環(huán)境的隨機(jī)模型，在運(yùn)行時(shí)監(jiān)測(cè)更新模型并通過對(duì)模型的形式分析來引導(dǎo)系統(tǒng)控制回路進(jìn)行決策。文獻(xiàn)[20，21]將運(yùn)行時(shí)定量驗(yàn)證（runtime quantitative verification，RQV）的概念引入到了自適應(yīng)系統(tǒng)驗(yàn)證領(lǐng)域中，并分別在遠(yuǎn)程醫(yī)療服務(wù)系統(tǒng)[22]和云計(jì)算基礎(chǔ)設(shè)施[23]等場(chǎng)景中進(jìn)行應(yīng)用。Mason等人[24]使用抽象策略定義系統(tǒng)中agent行為空間的區(qū)域，結(jié)合RQV來識(shí)別滿足約束的行為策略。Gadelha等人[25]提出使用場(chǎng)景作為運(yùn)行時(shí)實(shí)體來驗(yàn)證SAS的方法，該方法通過監(jiān)測(cè)系統(tǒng)運(yùn)行軌跡和場(chǎng)景之間的轉(zhuǎn)移概率來構(gòu)成系統(tǒng)行為規(guī)范，再通過RQV判斷出違反規(guī)范的系統(tǒng)行為。

隨著SAS的應(yīng)用場(chǎng)景越來越復(fù)雜、功能目標(biāo)越來越多，這使SAS需要向協(xié)作和分布式方向發(fā)展以具有更好的并發(fā)性和容錯(cuò)性等良好特性[26]。因此，多agent系統(tǒng)（multiagent system，MAS）及其協(xié)作模式和分布式優(yōu)化技術(shù)引起了研究者的關(guān)注。針對(duì)MAS的可協(xié)作性，將agent根據(jù)功能與特征進(jìn)行區(qū)分，將特征、功能不同的agent稱為異構(gòu)agent[27]。而現(xiàn)有應(yīng)用RQV的研究所描述的自適應(yīng)系統(tǒng)都是基于同構(gòu)多agent系統(tǒng)，并沒有考慮到存在異構(gòu)多agent的自適應(yīng)系統(tǒng)，同時(shí)其缺乏對(duì)異構(gòu)agent之間協(xié)作邏輯的形式化描述。若要對(duì)異構(gòu)多agent自適應(yīng)系統(tǒng)進(jìn)行驗(yàn)證，就要解決異構(gòu)agent的形式化建模和協(xié)作邏輯描述問題。

文獻(xiàn)[14]同樣是將需要驗(yàn)證的對(duì)象實(shí)體形式化描述為具有隨機(jī)過程的模型并結(jié)合定量驗(yàn)證以驗(yàn)證系統(tǒng)的各項(xiàng)需求指標(biāo)。文獻(xiàn)[14]將具有隨機(jī)行為的agent構(gòu)建為馬爾可夫決策過程（Markov decision processes，MDP），并結(jié)合交替時(shí)間邏輯（alternatingtime logic， ATL）建立agent的檢查指標(biāo)，但驗(yàn)證的對(duì)象實(shí)體與本文不同且不考慮不同類型agent之間存在協(xié)作問題的情況。Gadelha等人以文本或者圖形形式表示場(chǎng)景以描述SAS的一組事件序列，再用場(chǎng)景之間的轉(zhuǎn)換概率表達(dá)SAS的行為規(guī)范并應(yīng)用模型檢查技術(shù)驗(yàn)證可達(dá)性屬性是否成立；與本文邏輯基本一致，但其驗(yàn)證的SAS需求存在一定的局限性，無法表達(dá)SAS的全部行為事件且需要大量的場(chǎng)景數(shù)據(jù)來支持驗(yàn)證結(jié)果的正確性。文獻(xiàn)[28]將基于模型檢查的形式化概率框架應(yīng)用到了基于機(jī)器學(xué)習(xí)的系統(tǒng)框架中，通過MDP建模非確定行為并基于獎(jiǎng)勵(lì)屬性生成最優(yōu)策略；但其提出的模型框架是基于單agent的，不涉及異構(gòu)agent和協(xié)作問題，構(gòu)建的概率模型主要針對(duì)機(jī)器學(xué)習(xí)中的再訓(xùn)練模塊，能夠表達(dá)的功能行為有限。Weyns等人[29]基于自適應(yīng)反饋控制循環(huán)MAPEK構(gòu)建驗(yàn)證模型，使用一組正確性屬性驗(yàn)證的模型來表示MAPEK的四個(gè)主要階段[30]；該方法結(jié)合具體場(chǎng)景下的SAS構(gòu)建的系統(tǒng)模型同時(shí)包含系統(tǒng)的功能行為和MAPEK的四個(gè)主要階段，可以在運(yùn)行時(shí)直接部署和執(zhí)行；但相比本文而言，其驗(yàn)證的模型并不涉及多agent的概念，并且不適用存在協(xié)同工作問題的多反饋循環(huán)系統(tǒng)。

總體來說，本文工作針對(duì)隨機(jī)環(huán)境下的多agent自適應(yīng)系統(tǒng)構(gòu)建其概率模型，聚焦于異構(gòu)agent之間的協(xié)作問題并提出形式化解決方案，結(jié)合模型檢查和RQV技術(shù)在運(yùn)行時(shí)部署執(zhí)行驗(yàn)證模型以確保系統(tǒng)的安全性和穩(wěn)定性。本文從概率時(shí)間自動(dòng)機(jī)（probabilistic timed automata，PTA）和動(dòng)態(tài)環(huán)境下的異構(gòu)多agent自適應(yīng)系統(tǒng)出發(fā)，結(jié)合RQV提出了基于概率時(shí)間自動(dòng)機(jī)的異構(gòu)多agent自適應(yīng)運(yùn)行時(shí)驗(yàn)證方法（PTAbased heterogeneous multiagent selfadaptation runtime verification，PMARV）。首先根據(jù)系統(tǒng)中的異構(gòu)agent構(gòu)建相應(yīng)的PTA模型，組合PTA模型將SAS描述為可驗(yàn)證的概率時(shí)間自動(dòng)機(jī)網(wǎng)絡(luò)模型（probabilistic timed automata network，PTAN），由此可以得到SAS的可驗(yàn)證概率模型；根據(jù)SAS中異構(gòu)agent的協(xié)作邏輯問題，制定合理的安全約束條件并將其形式化描述為PTA模型支持的模型語言，再融入到SAS的概率模型中；在運(yùn)行時(shí)部署融合安全約束條件的SAS概率模型到相應(yīng)的模型檢查工具中，驗(yàn)證系統(tǒng)運(yùn)行過程中狀態(tài)遷移流程的安全性；將SAS的功能行為形式化為時(shí)間時(shí)序邏輯公式，用于量化系統(tǒng)的任務(wù)目標(biāo)作為驗(yàn)證的評(píng)估標(biāo)準(zhǔn)；通過模型檢查和運(yùn)行時(shí)定量驗(yàn)證分析模型，并在發(fā)生違反需求情況時(shí)生成重新配置計(jì)劃。

以智能無人停車系統(tǒng)（intelligent unmanned parking system，IUPS）作為研究背景和實(shí)驗(yàn)場(chǎng)景，其在此前的工作中已有應(yīng)用[31]。該系統(tǒng)中主要有兩類智能機(jī)器人，一類是用于裝載并跨層運(yùn)輸車輛的升降機(jī)器人lift，另一類是自動(dòng)泊車機(jī)器人AGV。

本文的主要貢獻(xiàn)有：

a）提出了一種基于概率時(shí)間自動(dòng)機(jī)的異構(gòu)多agent自適應(yīng)運(yùn)行時(shí)驗(yàn)證方法（PTAbased heterogeneous multiagent selfadaptation runtime verification，PMARV）。通過該方法，可以將異構(gòu)agent分別形式化描述為單個(gè)PTA模型，其組合起來的模型網(wǎng)絡(luò)PTAN便可模擬整個(gè)多agent自適應(yīng)系統(tǒng)。

b）將異構(gòu)agent之間的協(xié)作邏輯融入到SAS概率模型中，提出了一種異構(gòu)agent之間協(xié)作交互的形式化描述方法。該方法將協(xié)作邏輯轉(zhuǎn)換為模型語言加入到SAS概率模型中，通過制定安全約束驗(yàn)證系統(tǒng)運(yùn)行過程的安全性，實(shí)驗(yàn)證明其能夠有效保障系統(tǒng)運(yùn)行的穩(wěn)定性。

c）將運(yùn)行時(shí)定量驗(yàn)證技術(shù)擴(kuò)展運(yùn)用至異構(gòu)多agent系統(tǒng)中，并量化系統(tǒng)的功能行為作為驗(yàn)證的指標(biāo)。實(shí)驗(yàn)對(duì)比原始系統(tǒng)和運(yùn)用了運(yùn)行時(shí)定量驗(yàn)證的系統(tǒng)在運(yùn)行過程中的正確率，結(jié)果證明運(yùn)行時(shí)定量驗(yàn)證可以有效提高系統(tǒng)運(yùn)行的可靠性。

1 模型基礎(chǔ)與時(shí)序計(jì)算邏輯

1.1 時(shí)間自動(dòng)機(jī)模型

時(shí)間自動(dòng)機(jī)是帶有時(shí)鐘集的有限自動(dòng)機(jī)[32]，設(shè)X是一個(gè)有限的時(shí)鐘集合，其中x∈R∩[0，+∞]，表示記錄時(shí)間的時(shí)鐘變量。為時(shí)鐘變量賦值的動(dòng)作定義為時(shí)鐘變量到非負(fù)實(shí)數(shù)集的映射，記為X→R，R≥0。設(shè)C為一個(gè)由布爾變量組合的時(shí)鐘約束，若一個(gè)時(shí)鐘變量x的值滿足其時(shí)鐘約束C，則該時(shí)鐘約束C的結(jié)果為true，記為C==true，可以定義為以下幾種形式：

a）x≤n。

b）n≤x。

c）x1+n1≤x2+n2。

d）C。

e）C∩C。

其中：x1，x2，…，xi∈X;n1，n2都是自然數(shù)。如果C中存在的所有x都使C==true，則令C表示為時(shí)鐘變量集X上的時(shí)鐘約束集。

定義1 時(shí)間自動(dòng)機(jī)。一個(gè)時(shí)間自動(dòng)機(jī)可以定義為一個(gè)六元組TA=（S，s0，E，I，X，V）。其中：S是時(shí)間自動(dòng)機(jī)中所有狀態(tài)的非空集合；s0∈S是TA中所有初始狀態(tài)的集合；ES×C×Act×2C×S是一個(gè)狀態(tài)變遷的集合，Act是動(dòng)作a的集合；I：S→C是一個(gè)狀態(tài)集合與時(shí)鐘變量集合的映射，表示狀態(tài)的約束；X是一個(gè)有限的時(shí)鐘變量集合；V是數(shù)據(jù)變量的集合。

從狀態(tài)s到s′的轉(zhuǎn)換，記為（s，C，a，U，s′）∈E，該式表示當(dāng)處于狀態(tài)s時(shí)，只要滿足時(shí)鐘約束C，時(shí)間自動(dòng)機(jī)TA就可以執(zhí)行動(dòng)作a，U中的時(shí)鐘變量將被重新賦值，使?fàn)顟B(tài)由s轉(zhuǎn)移到s′的同時(shí)不違反I（s′）的時(shí)鐘約束。若時(shí)鐘約束I（s）持續(xù)被滿足，TA也可以停留在狀態(tài)s。

模型檢查是解決SAS驗(yàn)證問題的主要方法之一，其基本思想是以系統(tǒng)行為建立數(shù)學(xué)模型，然后基于模型進(jìn)行形式化分析[33]。時(shí)間自動(dòng)機(jī)是一種用于真實(shí)系統(tǒng)建模和驗(yàn)證的理論[34，35]，可將SAS的系統(tǒng)行為與結(jié)構(gòu)特征建模為時(shí)間自動(dòng)機(jī)模型進(jìn)行驗(yàn)證分析。然而，SAS需要根據(jù)環(huán)境的動(dòng)態(tài)變化作出適應(yīng)調(diào)整，其行為受不確定因素影響具有非確定性特征。因此，SAS的驗(yàn)證模型也需要具備分析不確定性因素的能力。而概率時(shí)間自動(dòng)機(jī)是一種具有不確定性和隨機(jī)性的形式化模型[36]，可以用于描述、分析帶有隨機(jī)因素實(shí)時(shí)系統(tǒng)行為，其定義在時(shí)間自動(dòng)機(jī)的基礎(chǔ)上進(jìn)行了擴(kuò)充。內(nèi)外環(huán)境中的不確定性是SAS不可避免的因素，為了更加有效地驗(yàn)證SAS的安全性，將這種隨機(jī)性融入驗(yàn)證工作中是及其必要的。假設(shè)SAS行為的某些特定方面可以用概率的形式描述，則可以將這類行為建模為一個(gè)隨機(jī)過程進(jìn)行驗(yàn)證，例如將來自系統(tǒng)環(huán)境中的不確定性抽象為概率形式，構(gòu)建成一個(gè)概率時(shí)間自動(dòng)機(jī)模型進(jìn)行驗(yàn)證分析。若系統(tǒng)中agent的某一種狀態(tài)存在多條轉(zhuǎn)移路徑時(shí)，可以將不同路線抽象為不同的隨機(jī)因素影響后的系統(tǒng)狀態(tài)變化路線，使其依照概率進(jìn)行狀態(tài)轉(zhuǎn)移。

定義2 概率時(shí)間自動(dòng)機(jī)。一個(gè)概率時(shí)間自動(dòng)機(jī)可以定義為一個(gè)六元組PTA=（S，s0，T，I，X，V）。其中S，s0，I，X和V與定義1中的意義相同。TS×C×Act×P（2C×S）是一個(gè)概率狀態(tài)變遷的集合；P（U，s′）：T→（0，1]是當(dāng)前狀態(tài)轉(zhuǎn)移到下一狀態(tài)的概率。

概率狀態(tài)的遷移可以記為（s，C，a，P）∈T，表示當(dāng)處于狀態(tài)s時(shí)，只要滿足時(shí)鐘約束C，概率時(shí)間自動(dòng)機(jī)PTA就可以執(zhí)行動(dòng)作a，U中的時(shí)鐘變量將被重新賦值，使?fàn)顟B(tài)以P（U，s′）的概率從s轉(zhuǎn)移到s′，與此同時(shí)不違反I（s′）的時(shí)鐘約束。與TA模型相同，若時(shí)鐘約束I（s）持續(xù)被滿足，PTA也可以停留在狀態(tài)s。

定義3 概率時(shí)間自動(dòng)機(jī)網(wǎng)絡(luò)。一個(gè)概率時(shí)間自動(dòng)機(jī)網(wǎng)絡(luò)可以定義為一個(gè)四元組PTAN=（（PTA），VG，Cl，Ch），其中：（PTA）=（PTA0，PTA1，PTA2，…，PTAn）是一組互相平行、互相關(guān)聯(lián)的概率時(shí)間自動(dòng)機(jī)；VG是全局變量的集合；Cl是全局時(shí)鐘的集合；Ch是同步信道的集合。

存在異構(gòu)多agent的SAS能夠適應(yīng)更加復(fù)雜的應(yīng)用場(chǎng)景，如何構(gòu)建異構(gòu)多agent的SAS模型則成為了其驗(yàn)證問題的難點(diǎn)。根據(jù)定義1與2，本文將SAS中的異構(gòu)agent分別建立為TA模型并將其面臨的不確定性因素抽象為概率形式，擴(kuò)展TA模型為PTA模型。由定義3可知，多個(gè)PTA模型可以組合成一個(gè)PTAN模型。多個(gè)同構(gòu)或異構(gòu)的agent共同組成了復(fù)雜SAS，則由多agent的PTA模型組成的PTAN模型便為SAS的可驗(yàn)證系統(tǒng)模型。

1.2 時(shí)間時(shí)序計(jì)算樹邏輯

在得到SAS的系統(tǒng)建模后，需要對(duì)系統(tǒng)模型進(jìn)行分析驗(yàn)證。時(shí)間時(shí)序邏輯（timed computation tree logic，TCTL）是一組時(shí)間性質(zhì)規(guī)約，可以用于形式化表示需要驗(yàn)證的系統(tǒng)屬性。其公式描述如表1所示。

表1中公式的語義定義為，字母A和E用于量化路徑。A表示給定的屬性應(yīng)該適用于樹的所有路徑，而E表示應(yīng)該至少有一個(gè)樹的路徑包含該屬性。符號(hào)[]和〈〉用于量化路徑中的狀態(tài)。[]表示路徑上的所有狀態(tài)都應(yīng)滿足該屬性，而〈〉表示執(zhí)行中至少有一個(gè)狀態(tài)滿足該屬性。E〈〉和A[]是一組對(duì)偶屬性，即E〈〉滿足當(dāng)且僅當(dāng)A[]不滿足。這種類型的屬性通常被歸類為安全屬性，即意味著系統(tǒng)在特定危險(xiǎn)不會(huì)發(fā)生的意義上是安全的。

通過TCTL構(gòu)建SAS的模型屬性檢查，可以對(duì)系統(tǒng)結(jié)構(gòu)屬性進(jìn)行初步的安全驗(yàn)證，而SAS中不確定的內(nèi)外環(huán)境因素可以通過對(duì)TCTL添加概率性質(zhì)的描述，得到TCTL的概率擴(kuò)展形式PTCTL（probabilistic timed computation tree logic）。采用PTCTL描述PTA系統(tǒng)模型的性質(zhì)，典型的例子有：

a）P<0.9[F<20 s send n]；

b）Trigger→P<0.000 1[G≤20deploy]；

c）Pmax=？[sent U fail]。

例a）的含義是在20 s內(nèi)發(fā)送n條message的概率小于0.9；例b）的含義為安全氣囊在觸發(fā)后20 ms內(nèi)未能展開的概率嚴(yán)格小于0.000 1，上述兩種公式通過驗(yàn)證后能夠得到一個(gè)布爾值，該值的含義為模型某些行為發(fā)生的概率是否高于或低于給定的界限；例c）的含義是在消息傳輸完成之前發(fā)生故障的最大概率是多少，該公式在進(jìn)行驗(yàn)證后得到的是一個(gè)概率值，該值表示某些行為的實(shí)際概率。

PTCTL的語法公式如下。

狀態(tài)公式：

：：=true|a|χ|∧||PΔp[ψ]|RrΔq（1）

路徑公式：

ψ：：=U≤k|U（2）

其中：a∈AP是原子命題，AP是原子命題集合；χ∈C（X）是一個(gè)時(shí)鐘約束；Δ∈{<，≤，≥，>}是一個(gè)關(guān)系運(yùn)算符；p∈Q∩[0，1];q∈Q≥0;r是一個(gè)獎(jiǎng)勵(lì)結(jié)構(gòu);k∈N。該計(jì)算樹邏輯在TCTL的基礎(chǔ)上擴(kuò)展出了概率算子（P）和獎(jiǎng)勵(lì)算子（R），PΔp[ψ]表示路徑公式為真的概率滿足概率界限P，RrΔq[ρ]表示獎(jiǎng)勵(lì)結(jié)構(gòu)r上的獎(jiǎng)勵(lì)函數(shù)ρ的期望值滿足其界限。

2 基于概率時(shí)間自動(dòng)機(jī)的多agent建模

2.1 PMARV框架

本文先對(duì)需要驗(yàn)證的SAS進(jìn)行建模，再通過模型驗(yàn)證平臺(tái)進(jìn)行驗(yàn)證。由于大型SAS所包含的任務(wù)目標(biāo)和agent類型多且復(fù)雜，還涉及到異構(gòu)agent之間的協(xié)作通信，所以如何對(duì)異構(gòu)多agent系統(tǒng)進(jìn)行建模是一個(gè)尤為重要的步驟。本文方法基于概率時(shí)間自動(dòng)機(jī)模型，因此采用的模型驗(yàn)證平臺(tái)為UPPAAL[37]，它可以對(duì)表現(xiàn)出概率行為的系統(tǒng)進(jìn)行建模和分析，其圖形化的交互界面使模型狀態(tài)直觀清晰。基于概率時(shí)間自動(dòng)機(jī)的SAS運(yùn)行時(shí)驗(yàn)證方法框架如圖1所示。

PMARV的步驟為：a）根據(jù)多agent自適應(yīng)系統(tǒng)中的功能業(yè)務(wù)區(qū)分出異構(gòu)agent，提取每個(gè)agent關(guān)鍵狀態(tài)以及引起狀態(tài)轉(zhuǎn)換的事件來表示SAS功能行為，得到SAS中每個(gè)agent的狀態(tài)轉(zhuǎn)移圖并為其構(gòu)造相應(yīng)的時(shí)間自動(dòng)機(jī)模型；b）將可能的隨機(jī)因素轉(zhuǎn)換為SAS中agent各狀態(tài)之間的轉(zhuǎn)移概率以模擬內(nèi)外環(huán)境對(duì)SAS的不確定性影響；c）根據(jù)agent狀態(tài)轉(zhuǎn)移圖與轉(zhuǎn)移概率，將全部agent的時(shí)間自動(dòng)機(jī)模型擴(kuò)展為具有不確定性因素的概率時(shí)間自動(dòng)機(jī)模型；d）在模型驗(yàn)證平臺(tái)中使用其支持的模型語言描述agent的概率時(shí)間自動(dòng)機(jī)模型并結(jié)合PTCTL公式對(duì)agent功能行為進(jìn)行形式化描述；e）在模型驗(yàn)證平臺(tái)中對(duì)載入的全部agent模型進(jìn)行分析驗(yàn)證，將得到的驗(yàn)證結(jié)果用于SAS在不確定環(huán)境下的決策，從而獲得滿足SAS服務(wù)質(zhì)量的規(guī)劃。

每一類模型檢查器在對(duì)模型進(jìn)行驗(yàn)證前都需要將抽象的時(shí)間自動(dòng)機(jī)模型描述為其所支持的模型語言，不同的模型檢查器使用不同的模型描述語言。UPPAAL可以將不同的模型建模在同一環(huán)境下，且多個(gè)模型間可通過guard、synchronisation和update等功能進(jìn)行同時(shí)跳轉(zhuǎn)和模型間的交互協(xié)作，因此可以將不同功能的異構(gòu)agent在同一環(huán)境下分別建模，通過guard（守衛(wèi)）進(jìn)行agent間的約束交互，通過synchronisation（同步）進(jìn)行協(xié)同狀態(tài)變遷，通過update（更新）進(jìn)行agent的數(shù)據(jù)更新，從而滿足多agent自適應(yīng)系統(tǒng)的整體功能。

2.2 異構(gòu)agent及其協(xié)作邏輯建模

復(fù)雜SAS中存在多種功能類型的異構(gòu)agent，異構(gòu)agent之間需要通過協(xié)作、通信等方式完成任務(wù)目標(biāo)。本節(jié)將闡述PMARV中步驟a）～c）的方法細(xì)節(jié)，具體到如何對(duì)異構(gòu)agent的協(xié)作邏輯以及合作方式進(jìn)行形式化描述。

2.2.1 agent協(xié)作邏輯

在復(fù)雜SAS中需要有不同類型的agent完成不同的任務(wù)目標(biāo)，一個(gè)任務(wù)目標(biāo)也可能需要多個(gè)agent共同參與。假設(shè)一個(gè)任務(wù)目標(biāo)需要A和B兩個(gè)agent先后合作完成，則A在執(zhí)行自己的任務(wù)時(shí)要和B進(jìn)行交互通信，確保B的狀態(tài)可以執(zhí)行交接后的任務(wù)，在任務(wù)交接時(shí)進(jìn)行安全檢查，使系統(tǒng)時(shí)刻處于安全可靠的狀態(tài)下，反之B對(duì)A也有同樣的協(xié)作邏輯。而agent之間需要進(jìn)行多少次協(xié)作通信以及協(xié)作時(shí)需要滿足什么樣的安全條件則由具體的任務(wù)目標(biāo)決定，將這種agent在環(huán)境中進(jìn)行的有一定持續(xù)時(shí)間的任務(wù)活動(dòng)稱為狀態(tài)，而agent等待、交互或檢查是一種特殊的狀態(tài)，本文稱其為協(xié)作邏輯。

定義4 agent協(xié)作邏輯。agent的協(xié)作邏輯L是一個(gè)七元組L=（S，s0，A，F(xiàn)，g，γ，P）。其中：S是時(shí)間自動(dòng)機(jī)中所有狀態(tài)的非空集合；s0∈S是初始狀態(tài)的集合；A∈Ｓ×Ｓ是所有狀態(tài)遷移的集合；F是agent相關(guān)邏輯表達(dá)式的集合；g：A→F表示每次狀態(tài)遷移需要滿足的條件，主要用于agent之間的安全檢查；γ是對(duì)環(huán)境變量的賦值；P：A→（0，1]是狀態(tài)轉(zhuǎn)移的概率。

agent的協(xié)作邏輯表示其狀態(tài)轉(zhuǎn)移邏輯，根據(jù)系統(tǒng)目標(biāo)的需求，一個(gè)agent可能需要多個(gè)協(xié)作邏輯，即其可能參與多個(gè)任務(wù)目標(biāo)的實(shí)現(xiàn)。同構(gòu)agent之間擁有相同的協(xié)作邏輯，不同的協(xié)作邏輯則決定了agent之間存在功能結(jié)構(gòu)的差異。本文將agent之間的交互通信行為稱為交互事件，交互事件由單個(gè)agent發(fā)起，可能有多個(gè)同構(gòu)或異構(gòu)的agent接收此事件。在交互事件中可以包含環(huán)境變量的更新，狀態(tài)屬性變量的調(diào)整以及轉(zhuǎn)移條件的檢查等多種交互。在2.2.2與2.2.3節(jié)中將會(huì)針對(duì)agent之間的交互事件與異構(gòu)多agent的協(xié)作方式進(jìn)行具體描述。

2.2.2 交互事件建模

事件是多個(gè)agent之間的交互協(xié)作，在概率時(shí)間自動(dòng)機(jī)模型中，可以采用廣播通道的方式表示agent之間的事件。對(duì)于系統(tǒng)整體而言，有全局廣播通道向多個(gè)agent發(fā)出交互信息；對(duì)于局部單個(gè)agent之間的交互，有單一廣播通道用于其交流協(xié)作，不同的廣播方式有不同的適應(yīng)場(chǎng)景，這將在下文中進(jìn)一步闡述。根據(jù)應(yīng)用場(chǎng)景下agent之間的通信協(xié)作方式，可以將交互事件分為更新事件和約束事件。設(shè)Eu為更新事件的集合，Ec為約束事件的集合。更新事件Eu的發(fā)起者一般為單個(gè)agent，接收者為單個(gè)或多個(gè)agent，會(huì)根據(jù)廣播消息更新自己狀態(tài)的相關(guān)變量。在更新事件的廣播信息發(fā)出或接收時(shí)，agent自身狀態(tài)可以保持不變，也可以在發(fā)出或接收后進(jìn)行狀態(tài)轉(zhuǎn)移。約束事件Ec一般由一個(gè)約束發(fā)起方和一個(gè)受約束方組成，約束發(fā)起方使受約束方的狀態(tài)在滿足一定約束條件前，不進(jìn)行狀態(tài)轉(zhuǎn)移或在受約束方的約束條件達(dá)成后一定進(jìn)行狀態(tài)轉(zhuǎn)移，在此期間通常會(huì)伴隨受約束方的Eu事件進(jìn)行。

設(shè)si，sj∈S，u∈Eu，u！和u？分別表示更新事件的發(fā)出和接收。當(dāng)agent發(fā)出或者接收更新事件時(shí)，如圖2左側(cè)update event部分表示，agent在狀態(tài)si發(fā)出更新事件u！，消息發(fā)出后agent可能仍然保持在狀態(tài)si，或者進(jìn)行狀態(tài)轉(zhuǎn)移至sj。接收更新事件同理，由于消息傳遞是瞬間完成的，所以事件發(fā)起或結(jié)束的agent狀態(tài)si需要將自動(dòng)機(jī)狀態(tài)屬性設(shè)置為committed，表示不消耗系統(tǒng)時(shí)間，這也表示消息傳遞是一種瞬時(shí)的過程。

在約束事件進(jìn)行的過程中，通常伴隨著更新事件的發(fā)出和接收，agent狀態(tài)屬性變量也因此產(chǎn)生變化。設(shè)agent之間的約束條件為R，則Ec∈Eu×C，設(shè)si，sj∈S，c！和c？表示約束事件的發(fā)出和接收。如圖2右側(cè)constraint event部分所示，agent在狀態(tài)sj發(fā)出約束事件c！，在狀態(tài)sm接收約束事件c？并判斷自身狀態(tài)是否滿足約束條件R。用條件三元運(yùn)算符表示約束條件的判定，τ與τ表示判定的結(jié)果，結(jié)果為τ時(shí)狀態(tài)一直保持在sm，直到約束判定結(jié)果為τ時(shí)，被約束的狀態(tài)一定轉(zhuǎn)移到sn。發(fā)出約束事件的狀態(tài)需要將自動(dòng)機(jī)狀態(tài)屬性設(shè)置為committed，表示不消耗系統(tǒng)時(shí)間。接收消息的狀態(tài)由于約束條件的達(dá)成會(huì)存在一定的時(shí)間需求，所以不需要設(shè)定自動(dòng)機(jī)狀態(tài)屬性。

2.2.3 異構(gòu)多agent建模

復(fù)雜場(chǎng)景下的SAS由多個(gè)agent組成，根據(jù)系統(tǒng)不同的功能需求，可以將agent分為多種結(jié)構(gòu)，完成相同功能目標(biāo)的agent有相同的協(xié)作邏輯。在模型中，將agent的協(xié)作邏輯用一個(gè)概率時(shí)間自動(dòng)機(jī)模型表達(dá)，一個(gè)agent對(duì)應(yīng)一個(gè)PTA模型，該agent的每次聲明實(shí)現(xiàn)則對(duì)應(yīng)該P(yáng)TA模型的實(shí)例化。

設(shè)AG為一個(gè)SAS中全部agent的集合，每個(gè)agk∈AG，agk表示協(xié)作邏輯為k的agent，k∈N。設(shè)對(duì)應(yīng)agk的概率時(shí)間自動(dòng)機(jī)元組為PTAk=（S，s0，T，I，X，V），其中時(shí)間自動(dòng)機(jī)的狀態(tài)、初始狀態(tài)、有向邊和狀態(tài)轉(zhuǎn)移的概率分別對(duì)應(yīng)agent協(xié)作邏輯中的狀態(tài)、初始狀態(tài)、狀態(tài)轉(zhuǎn)移和狀態(tài)轉(zhuǎn)移概率；agent協(xié)作邏輯中相關(guān)邏輯表達(dá)式及時(shí)間變量和的賦值則對(duì)應(yīng)時(shí)間自動(dòng)機(jī)中的X和V。協(xié)作邏輯中的g根據(jù)語義轉(zhuǎn)換為狀態(tài)不變式、狀態(tài)轉(zhuǎn)移中的觸發(fā)條件和動(dòng)作，其對(duì)應(yīng)時(shí)間自動(dòng)機(jī)中的I；時(shí)間自動(dòng)機(jī)每個(gè)狀態(tài)轉(zhuǎn)移中的賦值對(duì)應(yīng)協(xié)作邏輯中的γ函數(shù)賦值。

對(duì)于由單個(gè)agent或多個(gè)同構(gòu)agent組成的系統(tǒng)模型，該系統(tǒng)擁有一個(gè)統(tǒng)一的系統(tǒng)目標(biāo)，對(duì)應(yīng)agent擁有同一個(gè)協(xié)作邏輯，在這種情況下agent協(xié)作邏輯的狀態(tài)遷移基本是順序隨時(shí)間推移進(jìn)行的，不存在與其他agent的交互事件和復(fù)雜的隨機(jī)因素。對(duì)于由異構(gòu)agent組成的系統(tǒng)模型，可以確定系統(tǒng)中至少包含兩個(gè)及以上的功能目標(biāo)，需要由不同結(jié)構(gòu)的agent完成，其構(gòu)建的PTA模型可組成一個(gè)PTAN模型。多個(gè)agent共同實(shí)現(xiàn)系統(tǒng)目標(biāo)的方式可分為兩類。一類是agent之間先后交替順序完成任務(wù)目標(biāo)，如圖3所示，任務(wù)目標(biāo)task1、task2分別由agent1和agent2順序完成。agent1行為模式從si開始，在完成活動(dòng)task1后向agent2的狀態(tài)sj發(fā)起交互事件；agent2在狀態(tài)sj接收到事件后再完成目標(biāo)task2。另一類是單個(gè)agent發(fā)起，多個(gè)agent協(xié)作完成系統(tǒng)任務(wù)目標(biāo)task3，如圖4所示。agent1和agent2分別在初始狀態(tài)si和sm進(jìn)入活動(dòng)處理系統(tǒng)任務(wù)目標(biāo)task3，agent1是發(fā)起方，agent2是協(xié)作方，兩者都需要彼此的參與來完成任務(wù)目標(biāo)。

多agent自適應(yīng)系統(tǒng)的主要功能行為是通過其系統(tǒng)內(nèi)不同的agent完成的，可以說不同特征、不同功能的多個(gè)agent之間協(xié)作、適應(yīng)實(shí)現(xiàn)多種任務(wù)目標(biāo)就形成了一個(gè)系統(tǒng)，即多agent自適應(yīng)系統(tǒng)。因此，為系統(tǒng)中的每個(gè)agent都構(gòu)建其PTA模型，將這些PTA模型根據(jù)任務(wù)目標(biāo)組合起來，即可得到一個(gè)表示整個(gè)系統(tǒng)功能行為的PTAN模型。在模型檢查工具載入PTAN模型，結(jié)合RQV量化系統(tǒng)的任務(wù)目標(biāo)，即可在運(yùn)行時(shí)模擬系統(tǒng)的運(yùn)行過程并得出任務(wù)目標(biāo)的驗(yàn)證結(jié)果。

通過上述agent的建模方法，可以對(duì)復(fù)雜的異構(gòu)多agent自適應(yīng)系統(tǒng)進(jìn)行形式化建模。通過構(gòu)建agent之間的協(xié)作邏輯，可以初步確定系統(tǒng)中agent協(xié)作方式，具體到agent之間執(zhí)行任務(wù)的先后順序、所處狀態(tài)、何時(shí)開始執(zhí)行任務(wù)，以及是否需要其他agent滿足一定的先決條件等。確定協(xié)作方式是為后續(xù)協(xié)作邏輯的形式化描述做準(zhǔn)備。2.2.2節(jié)交互事件建模將agent之間的交互方式概括為了兩類，2.2.3節(jié)異構(gòu)agent建模將不同類型的agent參與執(zhí)行任務(wù)的方式概括為了兩類，并且都給出了PTA模型語言的描述表達(dá)，因此可以將其融入SAS的PTAN模型中，且不存在模型語言沖突的情況，解決了異構(gòu)多agent的協(xié)作問題和形式化問題。通過模擬運(yùn)行融入?yún)f(xié)作邏輯后的PTAN模型，即可對(duì)系統(tǒng)協(xié)作邏輯的安全性和RQV對(duì)系統(tǒng)可靠性的提升效果進(jìn)行分析和驗(yàn)證。

2.3 IUPS的多agent模型構(gòu)建

本節(jié)以IUPS為例，對(duì)上述方法進(jìn)行實(shí)例化。本文從IUPS中提取lift和AGV的關(guān)鍵狀態(tài)，lift的關(guān)鍵狀態(tài)如表2所示，AGV的關(guān)鍵狀態(tài)如表3所示。

在此前的工作中[28]已經(jīng)將IUPS環(huán)境因素的不確定性轉(zhuǎn)換為轉(zhuǎn)移概率并采用貝葉斯方法進(jìn)行計(jì)算。根據(jù)lift的故障集W=｛W1，W2，…，Wn｝和癥狀集E=｛E1，E2，…，Em｝構(gòu)建出圖5所示的雙層貝葉斯網(wǎng)絡(luò)。使用貝葉斯方法是為了計(jì)算出與agent狀態(tài)相對(duì)應(yīng)的故障概率值，即計(jì)算故障狀態(tài)節(jié)點(diǎn)的后驗(yàn)概率P（Wi|E）。

為了描述系統(tǒng)產(chǎn)生的不確定行為以及關(guān)鍵狀態(tài)之間發(fā)生的轉(zhuǎn)移，在模型中采用不同的符號(hào)對(duì)行為、狀態(tài)以及概率進(jìn)行描述。根據(jù)對(duì)PTAN的描述，系統(tǒng)中存在lift和AGV兩種不同功能的agent，其PTA模型可以組成一個(gè)概率時(shí)間自動(dòng)機(jī)網(wǎng)絡(luò)模型PTAN。定義IUPS的系統(tǒng)模型為一個(gè)四元組IUPS=（（PTA），VG，Cl，Ch），其中：概率時(shí)間自動(dòng)機(jī)集合PTA包含系統(tǒng)中的lift和AGV兩種PTA模型；VG、Cl與Ch分別是lift和AGV涉及的全局變量集合、全局時(shí)鐘集合和交互通信的通道集合。對(duì)于概率時(shí)間自動(dòng)機(jī)模型，這里以lift為例說明，lift的PTA模型為一個(gè)六元組lift=（S，s0，T，I，X，V），其中：

a）非空狀態(tài)集合S。模型中的狀態(tài)來源于系統(tǒng)運(yùn)行狀態(tài)，S包含兩類狀態(tài)S=｛Ni，F(xiàn)i｝，狀態(tài)Ni與系統(tǒng)正常運(yùn)行狀態(tài)一一對(duì)應(yīng)，狀態(tài)Fi表示系統(tǒng)運(yùn)行中發(fā)生的故障情況，用于表達(dá)不確定性。s0表示系統(tǒng)初始狀態(tài)。

b）概率狀態(tài)變遷集合T。描述了從lift狀態(tài)s轉(zhuǎn)移到狀態(tài)s′需要滿足的約束條件和轉(zhuǎn)移的概率，概率集合P中包含兩類轉(zhuǎn)移概率，pi表示系統(tǒng)正常運(yùn)行情況下的轉(zhuǎn)移概率，qi表示系統(tǒng)出現(xiàn)故障的轉(zhuǎn)移概率，而概率0用于表示該條轉(zhuǎn)移路徑無法通過。

c）數(shù)據(jù)變量集合V。用于標(biāo)記lift與AGV的狀態(tài)節(jié)點(diǎn)屬性，因此V是兩類agent中狀態(tài)節(jié)點(diǎn)屬性變量的集合。

結(jié)合所使用的IUPS場(chǎng)景構(gòu)建系統(tǒng)模型，可得到包含出現(xiàn)不確定情況的lift與AGV的PTA狀態(tài)轉(zhuǎn)移模型，以lift為例，其PTA狀態(tài)轉(zhuǎn)移模型如圖6所示。狀態(tài)Ni與系統(tǒng)運(yùn)行過程的正常狀態(tài)，狀態(tài)F1對(duì)應(yīng)不確定的故障狀態(tài)且有概率能轉(zhuǎn)移至正常運(yùn)行狀態(tài)。對(duì)于N0，其作為系統(tǒng)的初始狀態(tài)，由p0的概率轉(zhuǎn)移至N1且由q0的概率轉(zhuǎn)移至F1，由于N1與F1作為N0的輸出狀態(tài)，所以存在q0=1-p0；對(duì)于F1，其表示系統(tǒng)出錯(cuò)情況，在該狀態(tài)下，系統(tǒng)有概率p5轉(zhuǎn)移至正常狀態(tài)N1，也存在概率q5保持原狀以表示修復(fù)過程，有q5=1-p5。

3 實(shí)驗(yàn)過程及分析

本文以IUPS智能泊車系統(tǒng)場(chǎng)景為例，將RQV應(yīng)用于異構(gòu)多agent系統(tǒng)中，確定該技術(shù)在此領(lǐng)域中的適用性，并比較使用該技術(shù)后對(duì)系統(tǒng)的改善。智能無人停車系統(tǒng)具有運(yùn)行效率高、操作簡(jiǎn)便等特點(diǎn)，是現(xiàn)代城市化的重要發(fā)展方向之一。深圳某機(jī)器人公司近年投入并建設(shè)的無人停車系統(tǒng)運(yùn)用智能機(jī)器人運(yùn)輸和停放車輛，實(shí)現(xiàn)了智能泊車的目標(biāo)，并且部分項(xiàng)目已投入使用。本文實(shí)驗(yàn)基于上述應(yīng)用場(chǎng)景，構(gòu)建了面向無人環(huán)境的智能泊車系統(tǒng)的多agent場(chǎng)景并進(jìn)行了實(shí)驗(yàn)，本實(shí)驗(yàn)構(gòu)建的模型包含兩類異構(gòu)agent和一個(gè)獨(dú)立agent，異構(gòu)agent為lift和AGV，獨(dú)立agent為controller，用于輔助實(shí)驗(yàn)，方便對(duì)實(shí)驗(yàn)系統(tǒng)進(jìn)行調(diào)試。實(shí)驗(yàn)使用的仿真工具為UPPAAL 4.1.19，其是由Aaborg大學(xué)和Appsala大學(xué)聯(lián)合開發(fā)的模型仿真驗(yàn)證工具，支持對(duì)概率時(shí)間自動(dòng)機(jī)的模擬與仿真，被用于很多案例研究。4.1.19版本支持SMC方法，能夠在具有隨機(jī)語義的復(fù)雜實(shí)時(shí)系統(tǒng)的模型上進(jìn)行推理驗(yàn)證[38]。

實(shí)驗(yàn)1 IUPS異構(gòu)agent協(xié)作邏輯驗(yàn)證

為了驗(yàn)證異構(gòu)agent之間協(xié)作邏輯能否保障IUPS運(yùn)行過程的穩(wěn)定性，本實(shí)驗(yàn)首先將IUPS構(gòu)建為一個(gè)時(shí)間自動(dòng)機(jī)網(wǎng)絡(luò)模型，該模型網(wǎng)絡(luò)由lift和AGV構(gòu)建的時(shí)間自動(dòng)機(jī)模型組成。在本實(shí)驗(yàn)場(chǎng)景中，lift和AGV需要合作完成泊車的任務(wù)目標(biāo)，通過表2、3所描述的關(guān)鍵狀態(tài)，可以為智能泊車系統(tǒng)制定安全驗(yàn)證約束條件，如表4所示。將表中的約束條件形式化建模為agent協(xié)作邏輯中交互事件建模。將表中的前三條約束建模為agent之間約束事件交互模型，在滿足約束條件前agent狀態(tài)不能隨意變化。在系統(tǒng)運(yùn)行過程中，agent間的約束事件會(huì)伴隨著agent自身狀態(tài)屬性的變化，將狀態(tài)屬性變化建模為更新事件交互模型。表4中的第4、5條約束建模為更新事件，但處于其約束事件約束下。

將上述約束條件加入到構(gòu)建好的IUPS時(shí)間自動(dòng)機(jī)網(wǎng)絡(luò)模型中，為確保該模型能夠正常模擬IUPS在無人環(huán)境下的自主運(yùn)行，需要驗(yàn)證模型的系統(tǒng)邏輯和時(shí)序邏輯正確性，驗(yàn)證結(jié)果如表5所示。表中前兩行結(jié)果為lift與AGV的狀態(tài)可達(dá)性驗(yàn)證，證明了lift與AGV的各個(gè)關(guān)鍵狀態(tài)在模型中均處于正?？蛇_(dá)狀態(tài)。表中的屬性1～5與表4的序號(hào)相對(duì)應(yīng)，是將安全約束條件構(gòu)建為TCTL公式進(jìn)行驗(yàn)證。若驗(yàn)證性質(zhì)結(jié)果為滿足，說明安全約束條件成立，模型的運(yùn)行過程是安全的，其狀態(tài)遷移過程被限制在安全范圍內(nèi)，反之亦然，以此判斷安全約束條件的正確性。

在上述驗(yàn)證之后，模擬一組lift和AGV協(xié)作完成一次泊車任務(wù)的系統(tǒng)trace以驗(yàn)證模型運(yùn)行的完整流程，如圖7所示。controller為輔助系統(tǒng)整體運(yùn)行的agent，用于控制整個(gè)系統(tǒng)的開始與結(jié)束。圖中的數(shù)字0～5分別與表2、3中的序號(hào)相對(duì)應(yīng)，代表lift和AGV處于相應(yīng)的狀態(tài)。從圖7中可以看出，完成一次泊車任務(wù)，系統(tǒng)中兩類agent狀態(tài)轉(zhuǎn)移的路徑嚴(yán)格按照制定的安全約束進(jìn)行。本trace只模擬了任務(wù)完成一次的路徑，lift和AGV完成任務(wù)目標(biāo)后會(huì)回歸初始狀態(tài)并結(jié)束系統(tǒng)運(yùn)行，到達(dá)圖中黑色矩形的位置；若系統(tǒng)繼續(xù)運(yùn)行，則在完成一次任務(wù)后會(huì)進(jìn)入系統(tǒng)預(yù)備過程，再重新回到系統(tǒng)開始運(yùn)行的初始狀態(tài)，即圖中的黑色矩形會(huì)變?yōu)榘咨匦?，后續(xù)的系統(tǒng)trace與圖中保持一致。本實(shí)驗(yàn)驗(yàn)證了agent協(xié)作邏輯的正確性與其對(duì)系統(tǒng)運(yùn)行的影響，結(jié)果表明為異構(gòu)agent制定安全約束條件，也就是構(gòu)建agent協(xié)作邏輯中的交互事件模型，可以有效保證系統(tǒng)各狀態(tài)遷移的正確性。

實(shí)驗(yàn)2 IUPS正常狀態(tài)時(shí)長占比實(shí)驗(yàn)

為了研究RQV對(duì)異構(gòu)agent系統(tǒng)性能的改善，本實(shí)驗(yàn)應(yīng)用RQV的改進(jìn)系統(tǒng)與不使用RQV的原始系統(tǒng)進(jìn)行比較，并定義一段時(shí)間內(nèi)系統(tǒng)正常運(yùn)行的時(shí)間與該段時(shí)間的比值作為正確率以驗(yàn)證使用RQV后對(duì)系統(tǒng)性能的提升[28]。正確率越高表示系統(tǒng)性能越好。本實(shí)驗(yàn)在TA模型的基礎(chǔ)上加入概率形式的不確定因素，將時(shí)間自動(dòng)機(jī)模型TA調(diào)整為概率時(shí)間自動(dòng)機(jī)模型PTA并加入由實(shí)驗(yàn)1驗(yàn)證后的約束條件。將IUPS的任務(wù)目標(biāo)轉(zhuǎn)換為相應(yīng)的PTCTL公式并結(jié)合SMC統(tǒng)計(jì)方法在UPPAAL中進(jìn)行屬性驗(yàn)證。

將lift和AGV運(yùn)行過程中采集到的錯(cuò)誤數(shù)據(jù)作為癥狀集的先驗(yàn)概率，取故障集的先驗(yàn)概率為0.1。本文延用此前工作中l(wèi)ift和AGV的故障節(jié)點(diǎn)后驗(yàn)概率，如表6所示。qi代表系統(tǒng)在正常運(yùn)行狀態(tài)中發(fā)生故障的概率。qi的值越大，agent發(fā)生故障的概率越大。根據(jù)qi可知pi=1-qi，表示Ni轉(zhuǎn)移至Ni+1的概率值。對(duì)于以Fi為起點(diǎn)的自循環(huán)狀態(tài)，實(shí)驗(yàn)統(tǒng)一取值為qi+4=0.1，因此Fi狀態(tài)轉(zhuǎn)移至Ni狀態(tài)的概率為pi+4=0.9。

IUPS系統(tǒng)包含lift和AGV兩類agent，先分別比較RQV對(duì)每類agent的性能提升，再比較RQV對(duì)整體系統(tǒng)性能的提升。因?yàn)閷?duì)單個(gè)agent獨(dú)立進(jìn)行實(shí)驗(yàn)不涉及多個(gè)agent之間的協(xié)作，所以不需要加入安全約束。實(shí)驗(yàn)分別以liftRQV和AGVRQV的形式表示使用了RQV的改進(jìn)系統(tǒng)，以liftoriginal和AGVoriginal表示未使用RQV的原始系統(tǒng)。驗(yàn)證單個(gè)agent時(shí)，定義一段時(shí)間內(nèi)agent正常運(yùn)行的時(shí)間與該段時(shí)間的比值作為正確率以對(duì)比agent的性能優(yōu)劣。在UPPAAL中，每一個(gè)模擬時(shí)間對(duì)應(yīng)現(xiàn)實(shí)的1 s。本實(shí)驗(yàn)以500個(gè)模擬時(shí)間作為一個(gè)單位時(shí)間，得到兩類agent在10個(gè)單位時(shí)間內(nèi)的實(shí)驗(yàn)結(jié)果，分別如圖8、9所示。從圖中可以看出，在采用了RQV后兩類agent的正確率相比未使用RQV的原始系統(tǒng)有較大提升，lift的正確率有23%左右的提高，AGV有26%左右的提高。由于AGV所遇到的故障更多，其原系統(tǒng)在正確率上的波動(dòng)較大，在使用了RQV后具有較為明顯的改善。lift運(yùn)行過程中所遇到的不確定性相對(duì)較少，因此在整體正確率上也略高。

在驗(yàn)證了RQV對(duì)單個(gè)agent的提升后，需要驗(yàn)證其對(duì)整體系統(tǒng)的提升，此時(shí)需要加入由實(shí)驗(yàn)1驗(yàn)證后的安全約束條件來保障系統(tǒng)運(yùn)行。用sysRQV表示使用了RQV的改進(jìn)系統(tǒng)，以sysoriginal表示未使用RQV的原始系統(tǒng)。以系統(tǒng)正確率作為驗(yàn)證屬性構(gòu)建PTCTL公式驗(yàn)證模型。驗(yàn)證結(jié)果如圖10所示，可以看出，使用RQV后整體系統(tǒng)正確率一直優(yōu)于原始系統(tǒng)，提高幅度約為21%。

本文在智能無人泊車系統(tǒng)實(shí)驗(yàn)場(chǎng)景的基礎(chǔ)上，首先對(duì)系統(tǒng)中多agent的協(xié)作邏輯進(jìn)行安全驗(yàn)證，通過制定安全約束，可以確保系統(tǒng)運(yùn)行過程中狀態(tài)遷移的正確性與穩(wěn)定性，但協(xié)作邏輯的安全驗(yàn)證在面對(duì)功能較為復(fù)雜的SAS場(chǎng)景中存在一定的局限性。隨著SAS功能行為的增加，異構(gòu)agent的數(shù)量也隨之增加，其中可能存在更多的交互事件和安全約束條件，且與驗(yàn)證的成本成正相關(guān)。因此在大型復(fù)雜的SAS場(chǎng)景中，能否制定出簡(jiǎn)潔高效的安全約束條件和交互邏輯是決定驗(yàn)證成本與效率的重要因素。

本文通過多組比較實(shí)驗(yàn)可以得到RQV在單個(gè)或多agent實(shí)驗(yàn)中均比不使用RQV有較大的提升。實(shí)驗(yàn)結(jié)果表明，本文PAARV方法在異構(gòu)多agent系統(tǒng)中的可行性，且在使用該方法后對(duì)系統(tǒng)可靠性具有較大的提升。但實(shí)驗(yàn)的效果與SAS場(chǎng)景中的實(shí)際數(shù)據(jù)有關(guān)，若實(shí)際數(shù)據(jù)不能良好反映SAS的實(shí)際情況，實(shí)驗(yàn)結(jié)果的可靠性可能會(huì)受到一定影響。

4 結(jié)束語

本文提出了一種基于概率時(shí)間自動(dòng)機(jī)模型的異構(gòu)多agent自適應(yīng)運(yùn)行時(shí)驗(yàn)證方法。首先針對(duì)復(fù)雜SAS的建模問題，將系統(tǒng)中不同功能結(jié)構(gòu)的agent建模為時(shí)間自動(dòng)機(jī)模型，再將內(nèi)外環(huán)境中的隨機(jī)因素抽象為系統(tǒng)模型的轉(zhuǎn)移概率，使時(shí)間自動(dòng)機(jī)模型擁有概率形式的隨機(jī)變化，從而轉(zhuǎn)換為概率時(shí)間自動(dòng)機(jī)模型，這樣由多個(gè)PTA構(gòu)成的PTAN可以模擬出隨機(jī)環(huán)境下SAS的運(yùn)行過程。針對(duì)系統(tǒng)中存在異構(gòu)agent的驗(yàn)證問題，先形式化描述agent之間的協(xié)作邏輯，再制定相應(yīng)的安全約束策略，在此基礎(chǔ)上確保系統(tǒng)運(yùn)行邏輯保持在安全狀態(tài)下，從而驗(yàn)證系統(tǒng)agent協(xié)作邏輯的正確性和可靠性。最后使用概率模型檢查技術(shù)對(duì)功能需求進(jìn)行定量化的驗(yàn)證，與原始系統(tǒng)進(jìn)行了比較，證明了本文方法的有效性。

本文方法的不足在于，系統(tǒng)在運(yùn)行過程中相比原始系統(tǒng)增加了運(yùn)行時(shí)模型驗(yàn)證的過程，而驗(yàn)證分析需要額外的計(jì)算過程，且與模型的規(guī)模成正比，若agent數(shù)量較大，可能會(huì)導(dǎo)致驗(yàn)證產(chǎn)生狀態(tài)空間擁擠，降低系統(tǒng)的決策效率，增加系統(tǒng)的運(yùn)行成本；在系統(tǒng)運(yùn)行過程中，若環(huán)境出現(xiàn)重大變化，模型結(jié)構(gòu)可能會(huì)出現(xiàn)部分失效，此時(shí)系統(tǒng)模型需要重新設(shè)計(jì)更新，拉低驗(yàn)證的效率。未來的研究?jī)?nèi)容會(huì)聚焦于上述問題，研究如何優(yōu)化模型的狀態(tài)空間，提高驗(yàn)證效率并應(yīng)用于更大型以及復(fù)雜的SAS中；研究模型的更新方法，考慮引入人的因素，將人的影響加入到系統(tǒng)控制循環(huán)中，保持模型對(duì)內(nèi)外環(huán)境的適應(yīng)性，或者研究模型的動(dòng)態(tài)更新方法，使系統(tǒng)能監(jiān)測(cè)到環(huán)境重大變化導(dǎo)致的模型問題，自行更新修復(fù)模型，保證系統(tǒng)驗(yàn)證結(jié)果的可靠性。

參考文獻(xiàn)：

[1]de Lemos R， Giese H， Müller H A，et al. Software engineering for selfadpaptive systems：a second research roadmap[M]//De Lemos R， Giese H， Müller H A， et al. Software Engineering for SelfAdaptive Systems Ⅱ.Berlin：Springer，2013：1-32.

[2]董孟高，毛新軍，郭毅，等.自適應(yīng)agent的設(shè)計(jì)和實(shí)現(xiàn)[J].計(jì)算機(jī)科學(xué)與探索，2011，5（3）：238-246.（Dong Menggao， Mao Xinjun， Guo Yi， et al. Design and implementation of selfadaptive agent[J].Journal of Frontiers of Computer Science and Technology，2011，5（3）：238-246.）

[3]Betty H C C， Kerstin I E， Martin G，et al. Using models at runtime to address assurance for selfadaptive systems[M]//Bencomo N， France R， Cheng B H C， et al. Models@run.Time.Cham：Springer，2014：101-136.

[4]Xu Chang， Cheung S C， Ma Xiaoxing ， et al. Adam： identifying defects in contextaware adaptation[J].Journal of Systems & Software，2012，85（12）：2812-2828.

[5]Wang Zhimin， Elbaum S， Rosenblum D S. Automated generation of contextaware tests[C]//Proc of the 29th International Conference on Software Engineering.Piscataway，NJ：IEEE Press，2007：406-415.

[6]Weyns D， Iftikhar M U， de la lglesia D G，et al. A survey of formal methods in selfadaptive systems[C]//Proc of Computer Science and Software Engineering.New York：ACM Press，2012：67-79.

[7]Jeff M， Tom M. Towards specification， modelling and analysis of fault tolerance in self managed systems[C]//Proc of International Conference on Software Engineering.New York：ACM Press，2006：30-36.

[8]Zhang Ji， Cheng B H C. Modelbased development of dynamically adaptive software[C]//Proc of the 28th International Conference on Software Engineering.New York：ACM Press，2006：20-28.

[9]Vassev E， Hinchey M. ASSL：a software engineering approach to autonomic computing[J].Computer，2009，42（6）：90-93.

[10]Weyns D， Malek S， Andersson J. FORMS： unifying reference model for formal specification of distributed selfadaptive systems[J].ACM Trans on Autonomous and Adaptive Systems，2012，7（1）：1-61.

[11]Clarke E M， Lerda F. Model checking： software and beyond[J].Journal of Universal Computerence，2008，13（5）：639-649.

[12]Kong W， Ogata K， Seino T， et al. A lightweight integration of theorem proving and model checking for system verification[C]//Proc of the 12th AsiaPacific Software Engineering Conference.Piscataway，NJ：IEEE Press，2005：59-66.

[13]Todman T， Luk W. Verification of streaming designs by combining symbolic simulation and equivalence checking [C]//Proc of the 22nd International Conference on Field Programmable Logic & Applications.Piscataway，NJ：IEEE Press，2012：203-208.

[14]Lomuscio A R， Pirovano E. Parameterised verification of strategic properties in probabilistic multiagent systems[C]//Proc of the 19th International Conference on Autonomous Agents and Multiagent Systems.New York：ACM Press，2020：762-770.

[15]劉瑋，何成萬，馮在文.面向不確定性的自適應(yīng)需求規(guī)劃算法研究[J].小型微型計(jì)算機(jī)系統(tǒng)，2014，35（2）：266-272.（Liu Wei， He Chengwan， Feng Zaiwen. Planning algorithms to address uncertainty in selfadaptive software requirements[J].Journal of Chinese Computer Systems，2014，35（2）：266-272.）

[16]Dobson S， Zambonelli F， Denazis S，et al. A survey of autonomic communications[J].ACM Trans on Autonomous & Adaptive Systems，2006，1（2）：223-259.

[17]Liu Yepang， Xu Chang， Cheung S C. AFChecker： effective model checking for contextaware adaptive applications[J].Journal of Systems & Software，2013，86（3）：854-867.

[18]Bartels B， Kleine M. A CSPbased framework for the specification， verification， and implementation of adaptive systems[C]//Proc of the 6th International Symposium on Software Engineering for Adaptive and SelfManaging Systems.New York：ACM Press，2011：158-167.

[19]趙天琪，趙海燕，張偉，等.基于模型的自適應(yīng)方法綜述[J].軟件學(xué)報(bào)，2018，29（1）：23-41.（Zhao Tianqi， Zhao Haiyan， Zhang Wei， et al. Survey of modelbased selfadaptation methods[J].Journal of Software，2018，29（1）：23-41.）

[20]Calinescu R， Kwiatkowska M. Using quantitative analysis to implement autonomic IT systems[C]//Proc of the 31st International Conference on Software Engineering.Piscataway，NJ：IEEE Press，2009：100-110.

[21]Epifani I， Ghezzi C， Mirandola R，et al. Model evolution by runtime parameter adaptation[C]//Proc of the 31st International Conference on Software Engineering.Piscataway，NJ：IEEE Press，2009：16-24.

[22]Calinescu R， Rafiq Y， Johnson K，et al. Adaptive model learning for continual verification of nonfunctional properties[C]//Proc of the 5th ACM/SPEC International Conference on Performance Engineering.New York：ACM Press，2014：87-98.

[23]Johnson K， Calinescu R， Kikuchi S. An incremental verification framework for componentbased software systems[C]//Proc of the 16th International ACM Sigsoft Symposium on ComponentBased Software Engineering.New York：ACM Press，2013：33-42.

[24]Mason G， Calinescu R， Kudenko D， et al. Assurance in reinforcement learning using quantitative verification[J].Advances in Hybridization of Intelligent MethodsSmart Innovation， Systems and Technologies，2017，85：71-96.

[25]Gadelha R， Vieira L， Monteiro D，et al. Scen@rist： an approach for verifying selfadaptive systems using runtime scenarios[J].Software Quality Journal，2020，28（3）：1303-1345.

[26]洪學(xué)志.COBOT：一個(gè)面向協(xié)作的自適應(yīng)系統(tǒng)軟件框架[D].南京：南京大學(xué)，2015.（Hong Xuezhi. COBOT：a software framework for collaborative selfadaptive systems[D].Nanjing：Nanjing University，2015.）

[27]李爽，劉瑋，吳坤，等.面向運(yùn)行時(shí)協(xié)作的異構(gòu)agent能力選擇與補(bǔ)償方法研究[J].煙臺(tái)大學(xué)學(xué)報(bào)：自然科學(xué)與工程版，2017，30（2）：6.（Li Shuang， Liu Wei， Wu Kun， et al. Runtimeoriented collaborative heterogeneous agents capability choosing and compensation[J].Journal of Yantai University：Natural Science and Engineering Edition，2017，30（2）：6.）

[28]Maria C， David G， Javier C，et al. A probabilistic model checking approach to selfadapting machine learning systems[C]//Proc of International Conference on Software Engineering and Formal Methods.Cham：Springer，2022：317-332.

[29]Weyns D， Iftikhar M U， Soderlund J. Do external feedback loops improve the design of selfadaptive systems？A controlled experiment[C]//Proc of the 8th International Symposium on? Software Engineering for Adaptive and SelfManaging Systems.Piscataway，NJ：IEEE Press，2013：3-12.

[30]Weyns D， Iftikhar U. ActivFORMS：a formally founded modelbased approach to engineer selfadaptive systems[J].ACM Trans on Software Engineering and Methodology，2023，32（1）：1-48.

[31]葉幸瑜，劉瑋，王寧，等.基于馬爾可夫模型的多agent自適應(yīng)在線驗(yàn)證[J].計(jì)算機(jī)應(yīng)用研究，2021，38（5）：1477-1481.（Ye Xingyu， Liu Wei， Wang Ning， et al. Multiagent adaptive runtime verification based on Markov model[J].Application Research of Computers，2021，38（5）：1477-1481.）

[32]Desel J， Reisig W， Rozenberg G. Timed automata： semantics， algorithms and tools[M]//Desel J， Reisig W， Rozenberg G. Lecture Notes in Computer Science.Berlin：Springer，2004：87-124.

[33]Kwiatkowska M， Norman G， Parker D. Advances and challenges of probabilistic model checking[C]//Proc of the 48th Annual Allerton Conference on Communication，Control，and Computing.Piscataway，NJ：IEEE Press，2010：1691-1698.

[34]Alur R， Dill D. Automata for modeling realtime systems[C]//Proc of International Colloquium on Automata，Languages and Programming.Berlin：Springer，1990：322-335.

[35]Alur R， Dill D L. A theory of timed automata[J].Theoretical Computer Science，1994，126（2）：183-235.

[36]Norman G， Parker D， Sproston J. Model checking for probabilistic timed automata[J].Formal Methods in System Design，2013，43（2）：164-190.

[37]Behrmann G， David A， Larsen K G. A tutorial on UPPAAL[M]//Bernardo M， Corradini F. Formal Methods for the Design of RealTime Systems.Berlin：Springer，2004：200-236.

[38]David A， Larsen K G， Legay A，et al. Uppaal SMC tutorial[J].International Journal on Software Tools for Technology Transfer，2015，17（4）：397-415.