楊文華 ,周 宇 ,黃志球

1(南京航空航天大學(xué) 計(jì)算機(jī)科學(xué)與技術(shù)學(xué)院,江蘇 南京 211106)

2(高安全系統(tǒng)的軟件開(kāi)發(fā)與驗(yàn)證技術(shù)工信部重點(diǎn)實(shí)驗(yàn)室(南京航空航天大學(xué)),江蘇 南京 211106)

3(軟件新技術(shù)與產(chǎn)業(yè)化協(xié)同創(chuàng)新中心,江蘇 南京 210093)

信息物理系統(tǒng)(cyber-physical system,簡(jiǎn)稱CPS)涵蓋了人、機(jī)、物的融合,它借助技術(shù)手段將人的控制延伸至信息與物理世界.CPS 涉及環(huán)境感知、嵌入式計(jì)算、網(wǎng)絡(luò)通信和控制等系統(tǒng)工程,其目標(biāo)是使物理系統(tǒng)具有計(jì)算、通信、精確控制、遠(yuǎn)程協(xié)作和自治能力.它注重計(jì)算資源與物理資源的緊密結(jié)合與協(xié)調(diào),其應(yīng)用領(lǐng)域非常廣泛,包括工業(yè)控制、智能制造、智能交通、遠(yuǎn)程醫(yī)療、智能電網(wǎng)、航空航天等領(lǐng)域[1].研究CPS 對(duì)于相關(guān)領(lǐng)域軟件的發(fā)展具有十分重要的意義.

CPS 需要融合像傳感器、嵌入式計(jì)算、云計(jì)算、網(wǎng)絡(luò)通信與軟件等各類信息技術(shù),設(shè)計(jì)時(shí)需要考慮如何對(duì)系統(tǒng)進(jìn)行智能、安全、高效的控制,以完成復(fù)雜、精密的應(yīng)用.與此同時(shí),信息計(jì)算、物理設(shè)備、外界環(huán)境之間的復(fù)雜交互也需要得到關(guān)注,因此CPS 往往比較復(fù)雜.除此之外,由于系統(tǒng)與環(huán)境的固有復(fù)雜性以及系統(tǒng)中使用設(shè)備的不完美性,不確定性普遍且固有存在于CPS 中.例如,系統(tǒng)感知環(huán)境時(shí)使用的傳感器就難免會(huì)存在誤差,這一誤差的具體值在運(yùn)行時(shí)是不確定的[2,3].然而,CPS 的“身影”又廣泛出現(xiàn)在大量安全與任務(wù)攸關(guān)領(lǐng)域,因此,如何在CPS 復(fù)雜性及不確定性影響下對(duì)其質(zhì)量進(jìn)行保障成為了CPS 研究的重點(diǎn)關(guān)注問(wèn)題.形式化驗(yàn)證是保障系統(tǒng)質(zhì)量的有效途徑之一,它可以提供嚴(yán)格的證明來(lái)驗(yàn)證系統(tǒng)在運(yùn)行過(guò)程中是否滿足要求的性質(zhì).現(xiàn)有工作在CPS 的驗(yàn)證問(wèn)題上取得了顯著進(jìn)展[4],對(duì)CPS 的安全性[5,6]及魯棒性[7]等性質(zhì)進(jìn)行了驗(yàn)證.在這些驗(yàn)證工作中,模型檢驗(yàn)技術(shù)是一類被廣泛使用的技術(shù)[8].基于系統(tǒng)的模型與待檢驗(yàn)的規(guī)約性質(zhì),模型檢驗(yàn)技術(shù)可以自動(dòng)化地對(duì)系統(tǒng)模型的狀態(tài)空間進(jìn)行顯式的遍歷或者以符號(hào)化的不動(dòng)點(diǎn)計(jì)算來(lái)判斷該模型的行為是否滿足規(guī)約性質(zhì).當(dāng)檢查結(jié)束時(shí),如果未出現(xiàn)反例,則該模型對(duì)于此規(guī)約性質(zhì)而言一定是正確的;而如果出現(xiàn)反例,則模型檢驗(yàn)技術(shù)會(huì)給出一個(gè)具體的執(zhí)行軌跡,說(shuō)明模型是在何種輸入下如何一步步執(zhí)行并最終違反給定的規(guī)約性質(zhì)的.

不確定性廣泛存在于CPS 中且會(huì)影響系統(tǒng)的執(zhí)行.因此,在對(duì)CPS 驗(yàn)證時(shí)也需要考慮不確定性,否則會(huì)導(dǎo)致驗(yàn)證結(jié)果不準(zhǔn)確,與系統(tǒng)實(shí)際運(yùn)行情況存在偏差.一種通用處理不確定性的方法是對(duì)系統(tǒng)中的不確定性進(jìn)行建模,刻畫(huà)系統(tǒng)中不確定性的特性和影響,再在驗(yàn)證時(shí)融合系統(tǒng)模型與不確定性模型.例如,我們之前的工作[4,9]提出通過(guò)誤差區(qū)間與分布對(duì)CPS 中的不確定性(如傳感器感知誤差)進(jìn)行建模,之后借助約束求解器對(duì)系統(tǒng)進(jìn)行驗(yàn)證,驗(yàn)證時(shí)將不確定性對(duì)系統(tǒng)感知變量的影響考慮進(jìn)去.通過(guò)考慮這些不確定性,我們發(fā)現(xiàn)了已有驗(yàn)證方法不能發(fā)現(xiàn)的但系統(tǒng)實(shí)際運(yùn)行中卻存在的錯(cuò)誤情況(反例),提高了驗(yàn)證結(jié)果的準(zhǔn)確度.反例描繪了系統(tǒng)是在何種輸入下如何一步步執(zhí)行并違反規(guī)約的.但是由于受不確定性因素的影響,即使在給定的輸入下反例也不一定能夠被觸發(fā),因?yàn)槲覀儫o(wú)法控制不確定性的程度,比如報(bào)告的反例中要求傳感器的誤差是某個(gè)值,但系統(tǒng)在實(shí)際運(yùn)行時(shí)傳感器的誤差卻不一定滿足反例的觸發(fā)條件.因此,反例的發(fā)生是存在概率的,為此我們提出了一種估算反例發(fā)生概率的方法,可以提供更豐富的驗(yàn)證結(jié)果信息.

然而,驗(yàn)證的一個(gè)關(guān)鍵輸入是不確定性模型,這些驗(yàn)證工作的有效性非常依賴于不確定性模型是否精確.倘若輸入的不確定性模型不夠精確,則勢(shì)必會(huì)導(dǎo)致驗(yàn)證結(jié)果與實(shí)際不符.例如,我們使用誤差區(qū)間與分布來(lái)刻畫(huà)CPS 中的傳感器誤差這一不確定性,但是由于傳感器的運(yùn)行受眾多環(huán)境因素的影響以及數(shù)據(jù)樣本大小的局限性,實(shí)際中可能難以在最初就精確且完全地建模出這一不確定性,具體可以表現(xiàn)為誤差區(qū)間不精確或者分布的參數(shù)有偏差.驗(yàn)證時(shí)使用不精確的不確定性模型會(huì)影響驗(yàn)證結(jié)果的準(zhǔn)確度,比如報(bào)告的反例在現(xiàn)實(shí)中不會(huì)發(fā)生或者不太重要的反例可能被錯(cuò)誤地突出報(bào)告(像低概率的反例被報(bào)告為高概率).為了消除不精確的不確定性模型對(duì)驗(yàn)證結(jié)果的影響,我們提出通過(guò)校準(zhǔn)來(lái)得到精確的不確定性模型,從而提高驗(yàn)證結(jié)果的準(zhǔn)確度.

首先,為了確認(rèn)不確定性模型是否精確,我們觀察到可以利用反例確認(rèn)來(lái)進(jìn)行判斷.所謂反例確認(rèn)就是讓系統(tǒng)在反例要求的環(huán)境中運(yùn)行,觀察該反例是否會(huì)在系統(tǒng)執(zhí)行中被觸發(fā).在反例的確認(rèn)過(guò)程中,如果我們發(fā)現(xiàn)所報(bào)告的反例的概率與實(shí)際確認(rèn)時(shí)統(tǒng)計(jì)的反例發(fā)生概率相差甚遠(yuǎn),則可以認(rèn)為不確定性模型不夠精確,因?yàn)椴淮_定性模型是計(jì)算反例概率的關(guān)鍵輸入.例如,假設(shè)我們報(bào)告的一個(gè)反例,根據(jù)不確定性模型計(jì)算的反例發(fā)生概率為0.2,但在實(shí)際環(huán)境中對(duì)其進(jìn)行確認(rèn)時(shí)經(jīng)過(guò)統(tǒng)計(jì)后發(fā)現(xiàn),執(zhí)行了100 次都沒(méi)有觀察到該反例的觸發(fā),則可以有足夠的理由認(rèn)為用于驗(yàn)證的不確定性模型不夠精確.其次,在確認(rèn)不確定性模型不精確之后,為了得到更準(zhǔn)確的驗(yàn)證結(jié)果,我們提出了一種對(duì)不確定性模型進(jìn)行校準(zhǔn)的方法.該方法利用反例確認(rèn)的結(jié)果來(lái)指導(dǎo)不確定性模型的校準(zhǔn).具體而言,就是將不確定性模型的校準(zhǔn)問(wèn)題化歸為一個(gè)搜索問(wèn)題,搜索的目標(biāo)是最小化反例的計(jì)算概率與確認(rèn)過(guò)程中的反例觸發(fā)的實(shí)際概率之間的差異.通過(guò)遺傳算法對(duì)該搜索問(wèn)題進(jìn)行求解,求解的過(guò)程中會(huì)不斷改變不確定性模型(如區(qū)間范圍以及分布的參數(shù))以使得反例的計(jì)算概率與實(shí)際概率的差異最小化,之后將滿足最小化的不確定模型作為校準(zhǔn)后的模型.為了進(jìn)一步確認(rèn)校準(zhǔn)后的不確定性模型是否精確,我們通過(guò)假設(shè)檢驗(yàn)來(lái)幫助判斷.我們使用校準(zhǔn)后的不確定性模型重新驗(yàn)證系統(tǒng),再對(duì)新報(bào)告的反例進(jìn)行確認(rèn)并對(duì)它們的計(jì)算概率與實(shí)際概率進(jìn)行假設(shè)檢驗(yàn)來(lái)判斷這兩種概率之間的差異是否足夠小.若能通過(guò)檢驗(yàn),則接受校準(zhǔn)后的不確定性模型并停止校準(zhǔn),否則,引入更多的反例確認(rèn)數(shù)據(jù),重復(fù)上述校準(zhǔn)過(guò)程,直至通過(guò)檢驗(yàn).

本文第1 節(jié)介紹我們所使用的驅(qū)動(dòng)案例,一個(gè)自動(dòng)避障與搜索小車(chē)系統(tǒng).第2 節(jié)詳細(xì)介紹我們提出的不確定性模型校準(zhǔn)方法.第3 節(jié)展示校準(zhǔn)方法在驅(qū)動(dòng)案例上的實(shí)驗(yàn)結(jié)果以及分析.第4 節(jié)介紹目前對(duì)CPS 中不確定性進(jìn)行處理的相關(guān)工作.最后第5 節(jié)是總結(jié).

1 驅(qū)動(dòng)案例

自動(dòng)小車(chē)是一類典型的信息物理系統(tǒng)[1].圖1 展示的是一個(gè)自動(dòng)小車(chē)系統(tǒng)的運(yùn)行場(chǎng)景.小車(chē)的主要功能是探索整個(gè)區(qū)域并避免碰撞到任何障礙物.小車(chē)可以在方格內(nèi)執(zhí)行相應(yīng)動(dòng)作,移動(dòng)到東南西北4 個(gè)方位的其他方格內(nèi).小車(chē)車(chē)身四周配備了傳感器,可以感知四周障礙物的距離.為了確認(rèn)小車(chē)對(duì)區(qū)域探索是否廣泛,區(qū)域內(nèi)設(shè)置了一些檢查點(diǎn),小車(chē)巡視到檢查點(diǎn)時(shí)會(huì)收到相應(yīng)信號(hào).自動(dòng)小車(chē)系統(tǒng)會(huì)基于感知到的距離來(lái)決定小車(chē)的探索動(dòng)作并躲避障礙物.如果小車(chē)撞到障礙物,則認(rèn)為自動(dòng)小車(chē)系統(tǒng)失效,或者小車(chē)的運(yùn)行步數(shù)超出了一個(gè)閾值卻仍未巡視到所有檢查點(diǎn),這種現(xiàn)象也認(rèn)為是失效.

小車(chē)系統(tǒng)的運(yùn)行邏輯是系統(tǒng)設(shè)計(jì)的關(guān)鍵,為了應(yīng)對(duì)這一問(wèn)題,我們的已有工作[4]提出了使用交互狀態(tài)機(jī)(interaction state machine,簡(jiǎn)稱ISM)來(lái)建模系統(tǒng)的運(yùn)行邏輯.ISM 被定義為一個(gè)元組M:=(S,V,R,s0),其中,S是系統(tǒng)所有狀態(tài)的集合,s0∈S是系統(tǒng)的初始狀態(tài);V是包含系統(tǒng)所有變量的集合.V=Vs∪Vn,其中,Vs和Vn表示兩個(gè)不相交的類別.Vs包含所有的感知變量,這些變量存儲(chǔ)系統(tǒng)關(guān)注的環(huán)境屬性值,Vn包含了其他所有變量,即非感知變量;R是系統(tǒng)所有執(zhí)行規(guī)則的集合.對(duì)于每個(gè)規(guī)則r∈R,r關(guān)聯(lián)到一個(gè)狀態(tài)s∈S,該狀態(tài)是r的源狀態(tài).規(guī)則r的形式是r:=(condition,actions),條件condition是一個(gè)邏輯公式,其涉及的變量都在V中,當(dāng)公式被滿足時(shí),規(guī)則會(huì)被觸發(fā)執(zhí)行.動(dòng)作actions規(guī)定了當(dāng)規(guī)則被觸發(fā)時(shí)應(yīng)該執(zhí)行的動(dòng)作,這些動(dòng)作可以更新系統(tǒng)狀態(tài)也可以與環(huán)境進(jìn)行交互(例如控制小車(chē)移動(dòng)).系統(tǒng)通過(guò)ISM 模型是可以執(zhí)行的.從初發(fā)狀態(tài)s0出發(fā),一個(gè)ISM 模型M:=(S,V,R,s0)重復(fù)地讀取其感知變量的值(自動(dòng)地通過(guò)傳感器的環(huán)境感知更新),然后評(píng)估并決定執(zhí)行何條規(guī)則,最后執(zhí)行被選中規(guī)則的相應(yīng)動(dòng)作.當(dāng)狀態(tài)s∈S是M的當(dāng)前狀態(tài)時(shí),以s為源狀態(tài)的所有規(guī)則被啟用,而其他規(guī)則被禁用.只有被啟用的規(guī)則可以參與到規(guī)則的評(píng)估中,評(píng)估是依據(jù)環(huán)境感知來(lái)判斷規(guī)則的邏輯公式是否被滿足.若一個(gè)被啟用的規(guī)則r的條件r.condition被滿足,則該規(guī)則將被觸發(fā)執(zhí)行.當(dāng)有多條規(guī)則的條件都得到滿足時(shí),只能有一條規(guī)則被選擇執(zhí)行,這可以通過(guò)一些優(yōu)先級(jí)或隨機(jī)機(jī)制來(lái)解決.因此,一個(gè)ISM 模型的一次執(zhí)行可以表示為一條由狀態(tài)和規(guī)則構(gòu)成的路徑σ=s0r1s1...rnsn.

Fig.1 The running scenario of the robot-car system圖1 自動(dòng)小車(chē)系統(tǒng)運(yùn)行場(chǎng)景

為了驗(yàn)證CPS 的行為是否正確,已有工作[4]基于ISM 使用模型檢驗(yàn)技術(shù)對(duì)系統(tǒng)進(jìn)行驗(yàn)證.具體而言,首先將ISM 模型中的路徑取出,獲取每條路徑的路徑條件(即路徑中所有規(guī)則的條件的合取).由于系統(tǒng)與環(huán)境之間存在交互動(dòng)作,系統(tǒng)執(zhí)行完這些交互動(dòng)作會(huì)影響系統(tǒng)后續(xù)的環(huán)境(例如小車(chē)往東移動(dòng)后,與東邊障礙物的距離會(huì)縮短),因此需要將這些動(dòng)作的效果建模出來(lái),具體可以建模為模型中感知變量之間的約束(例如小車(chē)往東移動(dòng)前后與東邊障礙物的距離之差應(yīng)為小車(chē)東移的距離).另外,為了考慮系統(tǒng)中的不確定性,使用誤差區(qū)間對(duì)其進(jìn)行建模.例如,假設(shè)小車(chē)與東邊障礙物的實(shí)際距離為east,但是受由于不確定性因素的影響,傳感器存在一個(gè)誤差區(qū)間[–6,6],因此小車(chē)感知到距離可能不是east,而是[east?6,east+6]范圍內(nèi)的某個(gè)值.在進(jìn)行驗(yàn)證時(shí),將路徑條件中受不確定性影響的感知變量v替換為v＇,同時(shí)要求它們滿足v–a≤v＇≤v+b這一約束,其中,[a,b]是傳感器的誤差區(qū)間.最后,將更新后的路徑條件、建模動(dòng)作效果的約束以及失效條件一起輸入到SMT(satisfiability modulo theories)約束求解器進(jìn)行求解.詳細(xì)的驗(yàn)證方法和過(guò)程可參見(jiàn)文獻(xiàn)[4,9],這里不再贅述.若約束不滿足,則說(shuō)明路徑正確,否則,說(shuō)明此路徑有問(wèn)題,約束求解器也會(huì)給出一個(gè)反例,描述此路徑對(duì)應(yīng)的約束中所有變量的取值情況.反例對(duì)應(yīng)的是系統(tǒng)的一次實(shí)際執(zhí)行.以小車(chē)系統(tǒng)為例,根據(jù)小車(chē)系統(tǒng)的反例可以構(gòu)造出一個(gè)實(shí)際的物理環(huán)境(如障礙物的分布).讓小車(chē)在這一環(huán)境中運(yùn)行,該反例卻不一定會(huì)被觸發(fā),因?yàn)閭鞲衅鞯牟淮_定性不受我們控制.因此,即使在反例對(duì)應(yīng)的環(huán)境中,反例的觸發(fā)也存在一定的概率.而這一概率與建模不確定性的誤差區(qū)間有著密切的聯(lián)系,不確定性在誤差區(qū)間內(nèi)如何分布會(huì)影響到反例的觸發(fā)概率.因此,在建模不確定性時(shí),不僅可以使用誤差區(qū)間還需要使用概率分布.例如,傳感器的誤差可以是高斯分布或者均勻分布.依據(jù)這些不確定性模型以及系統(tǒng)模型,可以計(jì)算出所報(bào)告的反例的發(fā)生概率.反例概率描述的是在給定的輸入下(以小車(chē)為例,即一個(gè)障礙物分布的具體實(shí)際場(chǎng)景),系統(tǒng)按照該反例規(guī)定的路徑執(zhí)行的概率.在這一過(guò)程中,我們不要求反例中某些變量的取值(例如運(yùn)行時(shí)感知的誤差)與驗(yàn)證時(shí)返回的值一致.文獻(xiàn)[9]的工作中也給出了詳細(xì)的計(jì)算方法.這些驗(yàn)證結(jié)果的信息非常豐富,可以為系統(tǒng)質(zhì)量的提高和改善提供巨大的幫助.

可以看出,在這一驗(yàn)證過(guò)程中,不確定性模型起著至關(guān)重要的作用.不確定性模型不僅會(huì)影響報(bào)告反例的數(shù)量,還會(huì)影響反例的計(jì)算概率.以上述小車(chē)系統(tǒng)為例,傳感器的誤差范圍實(shí)際應(yīng)該為[–6,6],但在最初可能會(huì)得到[–5,5]這樣一個(gè)范圍.若驗(yàn)證時(shí)使用的是這樣一個(gè)不精確的模型,顯然會(huì)導(dǎo)致驗(yàn)證結(jié)果不準(zhǔn)確,比如無(wú)法報(bào)告實(shí)際存在的反例.除此之外,建模不確定性的概率分布得也可能不精確.假設(shè)不確定性的實(shí)際概率分布為均值是0、方差為1 的高斯分布N(0,1),但最初建模時(shí)無(wú)法精確獲得相關(guān)信息,使用的是均值為0、方差為4 的高斯分布N(0,4).由于估算反例發(fā)生概率時(shí)會(huì)用到不確定性的概率分布,使用這一不精確的模型,顯然會(huì)導(dǎo)致反例概率的計(jì)算不夠準(zhǔn)確.因此,為了得到更準(zhǔn)確的驗(yàn)證結(jié)果,需要對(duì)不精確的不確定性模型進(jìn)行校準(zhǔn).

2 基于反例確認(rèn)的模型校準(zhǔn)方法

為了獲取更準(zhǔn)確的驗(yàn)證結(jié)果,我們的已有工作在驗(yàn)證CPS 時(shí)考慮了系統(tǒng)中的不確定性[9].相較其他驗(yàn)證方法,該方法可以檢測(cè)到許多被其他方法忽略的真實(shí)反例.而該驗(yàn)證方法的一個(gè)重要輸入是不確定性模型.建模不確定性時(shí)使用的是物理學(xué)中常用的誤差區(qū)間與分布.以傳感器感知的不確定性為例,在感知時(shí)傳感器不可避免地存在誤差,運(yùn)行時(shí)我們卻無(wú)法確認(rèn)具體的誤差值是多少.但這個(gè)誤差一般存在一個(gè)大概的范圍且常?？梢杂媚撤N分布對(duì)其進(jìn)行刻畫(huà).

然而,由于測(cè)量過(guò)程中不可控制的噪聲和數(shù)據(jù)樣本數(shù)量存在一定的局限性,很難在最初就精確而完整地建模系統(tǒng)中的不確定性[10].從而使得用于驗(yàn)證的不確定性模型不精確.這里,不確定性模型具體代表建模不確定性時(shí)所用的誤差區(qū)間與相關(guān)分布的一些參數(shù)(如高斯分布的均值和方差).而這些不精確的模型會(huì)導(dǎo)致驗(yàn)證結(jié)果偏離現(xiàn)實(shí):不太重要的反例可能被錯(cuò)誤地突出顯示(如本來(lái)低概率的反例變成了高概率),或者更糟的是,還有可能會(huì)報(bào)告一些錯(cuò)誤的反例(如現(xiàn)實(shí)中不會(huì)發(fā)生).具體的表現(xiàn)形式可以是,所報(bào)告的反例的概率與實(shí)際中統(tǒng)計(jì)的反例發(fā)生的概率相差甚遠(yuǎn),因?yàn)椴淮_定性模型是計(jì)算反例概率的關(guān)鍵輸入.不精確的不確定性模型會(huì)導(dǎo)致所報(bào)告的反例的計(jì)算概率與真實(shí)場(chǎng)景中統(tǒng)計(jì)的實(shí)際概率之間出現(xiàn)不一致.基于這一關(guān)鍵觀察,我們提出通過(guò)反例確認(rèn),比較反例計(jì)算概率和執(zhí)行中統(tǒng)計(jì)的實(shí)際概率之間的差異來(lái)發(fā)現(xiàn)不精確的不確定性模型,并基于反例確認(rèn)的結(jié)果來(lái)進(jìn)行模型的校準(zhǔn).接下來(lái),我們將詳細(xì)介紹所提出的不確定性模型校準(zhǔn)方法.

2.1 方法概述

本節(jié)給出不確定性模型校準(zhǔn)方法的概述,我們將校準(zhǔn)問(wèn)題表達(dá)為一個(gè)搜索問(wèn)題,其目標(biāo)是最小化反例的計(jì)算概率與實(shí)際概率之間的差異.方法的過(guò)程如圖2 所示,主要包括識(shí)別、搜索以及判斷這3 部分.首先,為了識(shí)別不確定性模型是否精確,比較反例的計(jì)算概率與實(shí)際概率之間的差異,如果它們之間的差異很大(大于給定的閾值),則認(rèn)為不確定性模型是不精確的.在搜索階段,采用基于搜索的算法來(lái)找到最小化適應(yīng)度函數(shù)的解(即校準(zhǔn)了的不確定性模型).基于搜索的算法可以根據(jù)現(xiàn)有的數(shù)據(jù)集提供自動(dòng)評(píng)估,以評(píng)估校準(zhǔn)的不確定性模型的質(zhì)量.然而,仍然存在這些數(shù)據(jù)不具有代表性的可能,這將會(huì)導(dǎo)致校準(zhǔn)的不確定性模型與這些特定數(shù)據(jù)過(guò)于匹配從而偏離了真實(shí)的不確定性模型.為了應(yīng)對(duì)這個(gè)問(wèn)題,我們采用假設(shè)檢驗(yàn)來(lái)輔助判斷校準(zhǔn)后的模型是否精確且具有代表性.具體而言,我們使用校準(zhǔn)后的不確定性模型再次對(duì)系統(tǒng)進(jìn)行驗(yàn)證以獲取新的反例.對(duì)新的反例,計(jì)算它們的發(fā)生概率并統(tǒng)計(jì)它們?cè)趯?shí)際場(chǎng)景中的實(shí)際發(fā)生概率,再通過(guò)假設(shè)檢驗(yàn)判斷反例的計(jì)算概率與實(shí)際概率之間的差異是否足夠小.若能通過(guò)假設(shè)檢驗(yàn),則接受校準(zhǔn)后的模型并停止校準(zhǔn).否則,引入更多的反例樣本進(jìn)行校準(zhǔn),并重復(fù)該過(guò)程,直到假設(shè)檢驗(yàn)認(rèn)可校準(zhǔn)后的不確定性模型.

Fig.2 Overview of the calibration approach of uncertainty models圖2 不確定性模型校準(zhǔn)方法概述

2.2 反例確認(rèn)

不精確的不確定性模型會(huì)導(dǎo)致驗(yàn)證結(jié)果偏離現(xiàn)實(shí).反之,通過(guò)對(duì)驗(yàn)證結(jié)果進(jìn)行確認(rèn),可以發(fā)現(xiàn)用于驗(yàn)證的不確定性模型是否精確.換言之,我們可以讓系統(tǒng)在反例對(duì)應(yīng)的實(shí)際場(chǎng)景下運(yùn)行,統(tǒng)計(jì)反例是否會(huì)觸發(fā)以及觸發(fā)的頻率.根據(jù)這些信息,可以獲得反例的實(shí)際發(fā)生概率.然后將反例的計(jì)算概率與實(shí)際概率進(jìn)行比較,就能識(shí)別出不確定性模型是否精確.

已有工作[4]通過(guò)遍歷CPS 對(duì)應(yīng)的ISM 模型的每條候選路徑來(lái)收集系統(tǒng)的行為,并獲取路徑的路徑條件,其中與環(huán)境相關(guān)的變量使用了誤差區(qū)間來(lái)引入不確定性.失效條件描述了系統(tǒng)的故障,通過(guò)把失效條件與路徑條件合取再使用SMT 求解器對(duì)條件進(jìn)行求解可以得到驗(yàn)證結(jié)果.如果條件滿足的話,則意味著系統(tǒng)會(huì)失效,而求解器返回的解與路徑一起組成一個(gè)反例.反例描述了系統(tǒng)的執(zhí)行軌跡,其中包含失效條件與路徑條件中變量的取值,這些值可以對(duì)應(yīng)到導(dǎo)致系統(tǒng)失效的環(huán)境輸入.

驗(yàn)證結(jié)果的準(zhǔn)確性對(duì)系統(tǒng)調(diào)試過(guò)程有很大的影響,因?yàn)椴粶?zhǔn)確的驗(yàn)證結(jié)果會(huì)誤導(dǎo)開(kāi)發(fā)人員調(diào)試時(shí)的意圖.在不準(zhǔn)確的驗(yàn)證結(jié)果中可能會(huì)有虛假的反例,或者不太重要的反例被錯(cuò)誤地突出報(bào)告.為了精化驗(yàn)證結(jié)果,確認(rèn)(validation)是一種自然而廣泛采用的方法.確認(rèn)反例必須在反例描述的環(huán)境設(shè)置下實(shí)際部署并運(yùn)行系統(tǒng),觀察系統(tǒng)是否遵循反例的路徑執(zhí)行并失效.反例中包含了豐富的信息,像系統(tǒng)每一步執(zhí)行的動(dòng)作以及相關(guān)輸入變量的取值.根據(jù)這些信息可以構(gòu)造出一個(gè)系統(tǒng)實(shí)際的運(yùn)行場(chǎng)景.例如,自動(dòng)小車(chē)系統(tǒng)的一個(gè)反例就可以對(duì)應(yīng)到一個(gè)實(shí)際的物理場(chǎng)景,包括障礙物的分布以及檢查點(diǎn)的位置等.下面我們以一個(gè)簡(jiǎn)單的示例來(lái)加以說(shuō)明,針對(duì)一個(gè)反例,如何構(gòu)造與之對(duì)應(yīng)的一個(gè)實(shí)際的場(chǎng)景.圖3 展示的是一個(gè)簡(jiǎn)化的反例及其與之對(duì)應(yīng)的場(chǎng)景.我們規(guī)定的性質(zhì)是要求小車(chē)不要撞上障礙物,由于這里我們主要關(guān)注的是如何根據(jù)反例構(gòu)造一個(gè)實(shí)際的環(huán)境,因此給出的并非一個(gè)完整的反例,實(shí)際的反例往往比這復(fù)雜且會(huì)違反性質(zhì).假設(shè)我們通過(guò)驗(yàn)證找到這樣一個(gè)反例,該反例的路徑如圖3 所示,其中包含一條規(guī)則r1.而r1.condition要求小車(chē)與北邊障礙物的距離大于2,r1.actions描述的動(dòng)作是往北移動(dòng)一個(gè)單元.針對(duì)這條路徑中包含的變量north,求解器返回的值為3.路徑以及變量取值構(gòu)成了一個(gè)反例,而對(duì)于這個(gè)反例,我們可以構(gòu)造出圖中所示的實(shí)際場(chǎng)景,在小車(chē)往北移動(dòng)之前,根據(jù)north的取值可知,距小車(chē)北邊3 單元有一障礙物,因此我們可以構(gòu)造出圖中所示的場(chǎng)景.

Fig.3 An example of the environment construction for a counter example圖3 反例對(duì)應(yīng)的環(huán)境構(gòu)造示例

反例中包含的信息十分豐富,根據(jù)反例如何構(gòu)造實(shí)際場(chǎng)景亦很直觀,因此這里不再贅述.而反例確認(rèn)就是讓系統(tǒng)在該反例對(duì)應(yīng)的實(shí)際場(chǎng)景下來(lái)運(yùn)行,觀察反例能否觸發(fā).在觀察的過(guò)程中,我們還可以記錄系統(tǒng)運(yùn)行的次數(shù)以及每一次的運(yùn)行情況,從而可以統(tǒng)計(jì)出反例的實(shí)際概率.若通過(guò)比較反例計(jì)算概率以及實(shí)際概率發(fā)現(xiàn)兩者之間的差異較大,則可以安全地判斷出不確定性模型不夠精確,需要進(jìn)一步校準(zhǔn).

2.3 校準(zhǔn)問(wèn)題求解

為了校準(zhǔn)不精確的不確定性模型,我們提出將校準(zhǔn)問(wèn)題轉(zhuǎn)化為一個(gè)搜索問(wèn)題.給定一組具有實(shí)際概率和計(jì)算概率的反例,搜索以已有驗(yàn)證中使用的不確定性模型作為起始點(diǎn),搜索能夠最小化適應(yīng)度函數(shù)的不確定性模型.而適應(yīng)度函數(shù)是關(guān)于反例的實(shí)際概率和計(jì)算概率之間的差異.更具體地,不確定性模型是使用誤差區(qū)間與分布進(jìn)行建模的,而這些又表征為具體的參數(shù),例如高斯分布的均值和方差.因此,搜索問(wèn)題的本質(zhì)就是找到最小化適應(yīng)度函數(shù)的不確定性模型參數(shù)的值.下面,我們?cè)敿?xì)介紹適應(yīng)度函數(shù)的定義以及所使用的搜索算法.

2.3.1 適應(yīng)度函數(shù)的定義

適應(yīng)度函數(shù)描述的是搜索問(wèn)題的目標(biāo),并通常根據(jù)相關(guān)的度量標(biāo)準(zhǔn)或?qū)傩远右远x.如前所述,校準(zhǔn)需要首先發(fā)現(xiàn)所選反例的計(jì)算概率和實(shí)際概率之間的不一致性.我們通過(guò)計(jì)算這兩種概率之間的差異,并使用其絕對(duì)值的總和除以反例的個(gè)數(shù)來(lái)描述不一致性的程度.由于我們的目標(biāo)是找到適當(dāng)?shù)恼`差區(qū)間和分布的參數(shù)值,使得所選擇的反例的計(jì)算概率與實(shí)際概率之間的不一致最小化,所以我們直接將上述計(jì)算不一致性的函數(shù)作為適應(yīng)度函數(shù).為了獲得反例的實(shí)際概率,我們讓系統(tǒng)在反例相應(yīng)的環(huán)境中運(yùn)行固定次數(shù),并統(tǒng)計(jì)反例的觸發(fā)次數(shù).那么觸發(fā)次數(shù)與總次數(shù)的比值就是反例實(shí)際的概率.由于反例的個(gè)數(shù)可能很多,所以獲取所有反例的實(shí)際概率可能是非常耗時(shí)與不實(shí)際的,所以我們只選擇了一部分反例來(lái)作為樣本.選擇反例的策略可以有很多,但是我們建議先選擇具有高概率的反例,這樣可以加快校準(zhǔn)過(guò)程.

設(shè)U=(u1,u2,...,um)是包含不確定性模型所有參數(shù)的一個(gè)向量,Θ={σ1,σ2,…,σn}是選擇的反例的集合.每一個(gè)u i∈U(1≤i≤m)可以是誤差區(qū)間的上下限或者表征概率分布的參數(shù),這些參數(shù)是在連續(xù)區(qū)間上取值的.例如,表征高斯分布的參數(shù)是均值和方差,表征均勻分布的參數(shù)是區(qū)間的下限和上限.每一個(gè)σi∈Θ(1≤i≤n)具有一個(gè)根據(jù)不確定性模型U計(jì)算得到的計(jì)算概率cali,還有一個(gè)從確認(rèn)過(guò)程中得到的實(shí)際概率acti.適應(yīng)度函數(shù)用于衡量所選反例的兩種概率cali和acti之間的差異,其定義如公式(1)所示.由于具有多個(gè)反例,我們使用反例概率差異的平均值作為適應(yīng)度函數(shù),其中,n是反例的個(gè)數(shù).適應(yīng)度函數(shù)是搜索的目標(biāo)指導(dǎo),在這里我們校準(zhǔn)問(wèn)題的目標(biāo)是最小化適應(yīng)度函數(shù)的值.

2.3.2 搜索算法

在基于搜索的軟件工程相關(guān)研究中有許多優(yōu)秀的搜索算法,如爬山算法、模擬退火和遺傳算法等.這些算法具有不同的特征,可用于不同的場(chǎng)景.例如爬山算法與模擬退火被認(rèn)為是局部搜索算法,它們每次參考一個(gè)候選解進(jìn)行操作,并在該候選解的附近選擇移動(dòng)[11,12].另一方面,遺傳算法被認(rèn)為是全局搜索算法,可以一次在搜索空間中抽取多個(gè)點(diǎn),相比局部算法提供了更強(qiáng)的魯棒性[13].因此,在我們的問(wèn)題中使用遺傳算法進(jìn)行搜索.遺傳算法的過(guò)程從一組隨機(jī)選擇或預(yù)定義的個(gè)體開(kāi)始,它們組成了第1 代種群.之后,種群可以通過(guò)重復(fù)地選擇、交叉和變異等操作進(jìn)化以找到取得最優(yōu)值的個(gè)體.而評(píng)估個(gè)體與最優(yōu)解的接近程度是使用一個(gè)適應(yīng)度函數(shù).設(shè)計(jì)遺傳算法有幾個(gè)關(guān)鍵組成部分,如選擇操作(即如何選擇個(gè)體進(jìn)行復(fù)制)、交叉操作(即如何從兩個(gè)父代生成子代)、變異操作(即如何變異一個(gè)子代)和初始種群生成(即如何生成第1 代種群).

我們使用遺傳算法求解校準(zhǔn)問(wèn)題,其過(guò)程如算法1 所示.算法的輸入包括不確定性模型U、選定的反例的集合Θ、作為算法中主迭代過(guò)程終止條件的一個(gè)整數(shù)n和一個(gè)小實(shí)數(shù) .?算法生成一個(gè)固定個(gè)體數(shù)的初始種群,按照MATLAB 中給定的建議[14],當(dāng)適應(yīng)度函數(shù)中的變量數(shù)不大于5 個(gè)時(shí),初始種群數(shù)可以設(shè)為50,超過(guò)5 個(gè)時(shí)可以設(shè)為200 或者根據(jù)個(gè)數(shù)設(shè)成更多.種群規(guī)模也可以根據(jù)經(jīng)驗(yàn)進(jìn)行調(diào)整.增加種群數(shù)量使得遺傳算法能夠搜索更多的點(diǎn),從而獲得更好的結(jié)果.然而,種群規(guī)模越大,遺傳算法計(jì)算每一代的時(shí)間就越長(zhǎng).一種常見(jiàn)的生成初始種群中的個(gè)體的方法是從適應(yīng)度函數(shù)中的每個(gè)輸入變量(即U中的每個(gè)元素)的取值范圍內(nèi)隨機(jī)地選擇一個(gè)值.然而,這種方法忽略了已有的不確定性模型,盡管已有的模型在某種程度上并不精確,但仍然比隨機(jī)選擇的值具有更大的可信度.

算法1.基于遺傳算法的校準(zhǔn).

輸入:不確定性模型U,選擇的反例集合Θ,最大迭代次數(shù)n,閾值?(用于衡量?jī)纱芜B續(xù)評(píng)估值之間的差異);

輸出:校準(zhǔn)后的不確定性模型s.

換句話說(shuō),現(xiàn)有的不確定性模型是不精確的但并不是完全錯(cuò)誤的,所以要搜索的精確的不確定性模型應(yīng)該接近現(xiàn)有的模型.因此,我們基于現(xiàn)有的不確定性模型來(lái)生成初始種群.首先,將不確定性模型U中所有變量的值編碼成二進(jìn)制形式.之后,對(duì)于每一位以一個(gè)概率pm隨機(jī)地改變其值(從0 改為1 或從1 改為0),pm的取值后續(xù)將加以討論.算法的核心部分是其迭代過(guò)程(Lines 5～13),其中,種群進(jìn)行進(jìn)化并且個(gè)體依據(jù)它們的評(píng)估值被選擇.當(dāng)達(dá)到最大迭代次數(shù)n,或者種群的最佳評(píng)估值不再顯著變化(即兩個(gè)連續(xù)迭代的最佳評(píng)估值之間的差小于?)時(shí),搜索終止.然后,最適合的個(gè)體被解碼,以獲得輸入變量的值,它形成了校準(zhǔn)的不確定性模型.

在迭代過(guò)程中,有幾個(gè)關(guān)鍵的操作:選擇(Line 9)、交叉(Line 10)和變異(Line 11).下面我們?cè)敿?xì)加以介紹.

· 選擇.它根據(jù)評(píng)估值為子代個(gè)體選擇父代個(gè)體.對(duì)于每一個(gè)個(gè)體i,其評(píng)估值evali就是適應(yīng)度函數(shù)以個(gè)體i為不確定性模型的函數(shù)值fit.我們采用了一種標(biāo)準(zhǔn)的選擇方法(輪盤(pán)賭方法),其中,個(gè)體i被選擇的概率是evali是個(gè)體i的評(píng)估值,m是個(gè)體的總個(gè)數(shù).被選擇的個(gè)體都在選擇池中.

· 交叉.它通過(guò)交叉兩個(gè)父代個(gè)體來(lái)為新種群形成兩個(gè)新的子代個(gè)體.為了選擇交叉的父代,給定一個(gè)交叉概率pc,我們隨機(jī)地從選擇池中選擇pm×m/2 個(gè)父代.在具體的交叉操作中,單點(diǎn)交叉策略被應(yīng)用.然后,選擇池中父代被其子代所代替.

· 變異.它通過(guò)對(duì)種群中的個(gè)體進(jìn)行小的隨機(jī)改變來(lái)提供遺傳多樣性,并使遺傳算法能夠搜索更廣闊的空間.我們逐個(gè)地對(duì)選擇池中的個(gè)體加以選擇,并以變異概率pm隨機(jī)更改其字符(例如,將以二進(jìn)制形式編碼的個(gè)體的字符從0 改為1).

遺傳算法的參數(shù)(例如,交叉概率pc與變異概率pm)設(shè)置是問(wèn)題依賴的.一般來(lái)說(shuō),增大變異概率可能會(huì)增加遺傳的多樣性,但會(huì)導(dǎo)致搜索過(guò)于分散在解空間上,從而增大了交叉概率,可導(dǎo)致算法在解空間上相對(duì)集中的區(qū)域進(jìn)行搜索.我們也可以根據(jù)實(shí)驗(yàn)的反饋來(lái)調(diào)整參數(shù).同時(shí),現(xiàn)有的文獻(xiàn)總結(jié)了許多有價(jià)值的經(jīng)驗(yàn),供我們處理問(wèn)題時(shí)參考[15].根據(jù)建議,從[0.4,0.9]與[0.0001,0.1]中分別選擇交叉概率和變異概率的值是安全的.算法獲得的解包含了表示校準(zhǔn)的不確定性模型的參數(shù)變量的值.

2.4 假設(shè)檢驗(yàn)

在我們校準(zhǔn)不精確的不確定性模型之后,確定是否接受校準(zhǔn)的模型仍然是一個(gè)問(wèn)題,因?yàn)楸M管適應(yīng)度函數(shù)可以評(píng)估校準(zhǔn)的模型在現(xiàn)有數(shù)據(jù)樣本上的質(zhì)量,但該模型可能會(huì)過(guò)度匹配于這些數(shù)據(jù).為了解決這一挑戰(zhàn),我們引入了新的反例數(shù)據(jù)樣本,并采用假設(shè)檢驗(yàn)來(lái)幫助我們判斷在這個(gè)新的數(shù)據(jù)樣本中是否有足夠的證據(jù)來(lái)推斷校準(zhǔn)的不確定性模型對(duì)總體是精確的.假設(shè)檢驗(yàn)是用來(lái)判斷樣本與樣本、樣本與總體的差異是由抽樣誤差引起的還是本質(zhì)差別造成的統(tǒng)計(jì)推斷方法[16].其基本原理是先對(duì)總體的特征做出某種假設(shè),然后通過(guò)抽樣研究的統(tǒng)計(jì)推理,對(duì)此假設(shè)應(yīng)該被拒絕還是接受做出推斷.假設(shè)檢驗(yàn)檢查兩個(gè)對(duì)立的關(guān)于總體的假設(shè):原假設(shè)(H0)與備選假設(shè)(H1).原假設(shè)是待檢驗(yàn)的推斷.根據(jù)從樣本數(shù)據(jù)獲得的檢驗(yàn)統(tǒng)計(jì)量,測(cè)試確定是否接受或拒絕原假設(shè).就我們的問(wèn)題而言,想用假設(shè)檢驗(yàn)來(lái)回答的問(wèn)題是校準(zhǔn)的不確定性模型是否足夠精確.如前所述,有理由認(rèn)為,當(dāng)不確定性模型精確時(shí),反例的計(jì)算概率與實(shí)際概率之間不應(yīng)存在明顯的差異.基于該觀察,我們提出H0與H1.對(duì)于一組未用于校準(zhǔn)的反例σ1,σ2,...,σn,我們利用校準(zhǔn)后的不確定性模型計(jì)算每一個(gè)反例σi(1≤1≤n)的概率cali,并在實(shí)驗(yàn)中獲取其實(shí)際概率cati.如此一來(lái),便得到了n對(duì)獨(dú)立的觀察數(shù)據(jù):(cal1,act1),(cal2,act2),...,(caln,actn).設(shè)di(1≤1≤n)是σi的計(jì)算概率與實(shí)際概率之差,即di=cali–acti.由于每一個(gè)di都是由不確定性模型與精確的模型之間的偏差導(dǎo)致的,依據(jù)統(tǒng)計(jì)理論,則可以安全地假設(shè)它們服從一個(gè)正態(tài)分布.假設(shè)i=1,2,...,n,即d1,d2,...,dn是總體為的一個(gè)樣本,其中,未知.基于這個(gè)樣本,需要檢驗(yàn)假設(shè)H0:μd=0與H1:μd≠0.H0表示反例的計(jì)算概率和實(shí)際概率之間沒(méi)有顯著差異.相反地,H1表示它們之間存在顯著差異.下面,我們需要檢驗(yàn)是否可以接受H0.如果接受,我們可以有信心地得出結(jié)論:校準(zhǔn)的模型是足夠精確的,并據(jù)此停止校準(zhǔn)過(guò)程.否則,我們將引入更多的實(shí)驗(yàn)樣本來(lái)進(jìn)行校準(zhǔn),并重復(fù)校準(zhǔn)過(guò)程,直到假設(shè)檢驗(yàn)認(rèn)可校準(zhǔn)的不確定性模型.

我們?cè)诩僭O(shè)檢驗(yàn)中采用的是經(jīng)常使用的p值方法.p值被定義為在原假設(shè)成立的情況下獲得與實(shí)際觀察到的結(jié)果相同或“更極端”的概率.在此方法中,我們首先為原假設(shè)H0的p選擇一個(gè)閾值α,該值被稱為檢驗(yàn)的顯著性水平,一般設(shè)為5%或1%.如果p值小于或等于選定的顯著性水平(α),檢驗(yàn)表明觀察到的數(shù)據(jù)與原假設(shè)不一致,因此原假設(shè)應(yīng)該被拒絕.否則,接受原假設(shè).例如,使用一個(gè)常用的α=0.05,當(dāng)p＜0.05 時(shí)原假設(shè)被拒絕,當(dāng)p＞0.05 時(shí)接受原假設(shè).因此,p值的計(jì)算是我們假設(shè)檢驗(yàn)的關(guān)鍵步驟.為此,我們首先需要確定一個(gè)檢驗(yàn)統(tǒng)計(jì)量.存在許多檢驗(yàn)統(tǒng)計(jì)量(如paired tests、Z-tests、t-tests 和Chi-squared tests),其選擇是問(wèn)題依賴的.例如,Z-tests 適用于檢驗(yàn)嚴(yán)格服從正態(tài)分布且標(biāo)準(zhǔn)差已知的總體的均值.而t-tests 適用于在更寬松的條件下(假設(shè)更少)檢驗(yàn)均值.使用檢驗(yàn)統(tǒng)計(jì)量的觀察值與其已知的分布,即可以計(jì)算p值.例如,為了對(duì)一個(gè)服從高斯分布N(μ,σ2)(其中,σ未知)的總體的均值μ進(jìn)行假設(shè)檢驗(yàn),其中待檢驗(yàn)的假設(shè)是H0:μ=μ0,H1:μ≠μ0.我們使用被現(xiàn)有工作[16]廣泛采用的檢驗(yàn)統(tǒng)計(jì)量其中,是樣本的均值,S是樣本的標(biāo)準(zhǔn)差,n是樣本的數(shù)量.假設(shè)從樣本數(shù)據(jù)中計(jì)算的檢驗(yàn)統(tǒng)計(jì)量t的值是t0,則當(dāng)t0大于0 時(shí),p值等于,當(dāng)t0小于0 時(shí),p值等于許多現(xiàn)有的統(tǒng)計(jì)工具都支持p值的自動(dòng)計(jì)算.在我們的檢驗(yàn)中,也應(yīng)用相同的方法來(lái)計(jì)算p值.用與表示樣本d1,d2,...,dn的均值和方差.根據(jù)樣本的特性,我們也使用檢驗(yàn)統(tǒng)計(jì)量然后替換相應(yīng)的值得到.之后我們可使用上述討論的方法來(lái)計(jì)算其p值,并與顯著性水平α進(jìn)行比較,在我們的問(wèn)題中將其設(shè)為5%.如果p值大于α,則檢驗(yàn)表明反例的計(jì)算概率與實(shí)際概率之間沒(méi)有明顯的差異,故而可以接受原假設(shè).在這種情況下,我們接受校準(zhǔn)后的不確定性模型,并認(rèn)為其夠精確.如果p值不大于α,則檢驗(yàn)表明反例的計(jì)算概率與實(shí)際概率之間存在明顯的差異,應(yīng)該拒絕原假設(shè),不確定性模型也需要進(jìn)一步校準(zhǔn).這需要新的反例并獲取其計(jì)算概率和實(shí)際概率,這一過(guò)程可能是耗時(shí)的.不過(guò),幸運(yùn)的是,在假設(shè)檢驗(yàn)中,我們已經(jīng)有了一個(gè)新的反例樣本,顯然它們包含我們校準(zhǔn)所需的新的信息(計(jì)算概率與實(shí)際概率).因此,我們直接引入這些反例并重新校準(zhǔn)不確定性模型.

3 實(shí)驗(yàn)評(píng)估

本節(jié)評(píng)估校準(zhǔn)方法的有效性,具體考慮以下兩個(gè)研究問(wèn)題.

研究問(wèn)題1:我們的方法能不能有效地校準(zhǔn)不確定性模型?

研究問(wèn)題2:與其他算法相比,我們校準(zhǔn)中使用的遺傳算法表現(xiàn)如何?

在評(píng)估中我們使用第1 節(jié)介紹的驅(qū)動(dòng)案例作為實(shí)驗(yàn)對(duì)象.該CPS 使用ISM 進(jìn)行建模,詳細(xì)的ISM 模型取自文獻(xiàn)[4,9].借助已有工作中的驗(yàn)證方法,可以對(duì)該自動(dòng)小車(chē)系統(tǒng)進(jìn)行驗(yàn)證,獲取系統(tǒng)的反例并計(jì)算出這些反例的概率.

3.1 校準(zhǔn)的有效性

本實(shí)驗(yàn)評(píng)估的是采用我們的方法校準(zhǔn)CPS 中不精確的不確定性模型的有效性.為了評(píng)估校準(zhǔn)的有效性,我們首先需要得到不精確的不確定性模型,進(jìn)行校準(zhǔn)后再與精確的模型進(jìn)行對(duì)比.實(shí)驗(yàn)中,校準(zhǔn)的不精確的不確定性模型是在已有的一個(gè)精確的不確定性模型上改變得到的.在我們已有的工作[4]中,通過(guò)大量針對(duì)自動(dòng)小車(chē)系統(tǒng)的實(shí)驗(yàn)可以發(fā)現(xiàn),使用的一個(gè)已有的不確定性模型可以準(zhǔn)確地估算反例的概率.因此可以認(rèn)為這個(gè)已有的不確定性模型是足夠精確的,我們也用其作為實(shí)驗(yàn)中的精確的不確定性模型的基準(zhǔn).不精確的不確定性模型是在這個(gè)模型(誤差區(qū)間為[–6,6],分布為高斯分布N(0,22))的變化上得到的.

具體來(lái)說(shuō),我們識(shí)別了3 個(gè)控制變量:誤差區(qū)間以及分布的均值和方差.這些變量的變化是以每次改變一個(gè)變量的受控方式進(jìn)行的,我們對(duì)這些變量分別單獨(dú)增大或減小了±1 與±2,即每個(gè)變量都進(jìn)行了減小1 或2,增大1 或2 共4 種變化.通過(guò)一系列實(shí)驗(yàn)來(lái)檢查我們的方法是否可以成功地校準(zhǔn)那些不精確的不確定性模型.基于自動(dòng)小車(chē)系統(tǒng)的反例來(lái)校準(zhǔn)不精確的不確定性模型,自動(dòng)小車(chē)系統(tǒng)的每個(gè)反例都具有計(jì)算概率和實(shí)際概率.計(jì)算概率是用不精確的不確定性模型計(jì)算得到的,實(shí)際概率是從實(shí)驗(yàn)中統(tǒng)計(jì)獲得的.然后,將這些不精確的不確定性模型與反例一起傳遞給我們的校準(zhǔn)方法進(jìn)行校準(zhǔn).

表1 展示的是在驅(qū)動(dòng)案例上得到的實(shí)驗(yàn)結(jié)果.實(shí)驗(yàn)中,對(duì)于使用不精確的不確定性模型得到的反例進(jìn)行了確認(rèn),可以識(shí)別出這些反例的計(jì)算概率與實(shí)際場(chǎng)景中統(tǒng)計(jì)得到的實(shí)際概率之間差異較大,因此我們對(duì)其進(jìn)行了校準(zhǔn).我們將精確的不確定性模型作為評(píng)估校準(zhǔn)后模型的基準(zhǔn),而第2 列為校準(zhǔn)后的不確定性模型.為了比較兩個(gè)不確定性模型,使用歐氏距離來(lái)表示兩個(gè)模型之間的差異.誤差區(qū)間的下限l、上限u、均值n和方差v組成了模型m的4 個(gè)維度,兩個(gè)模型m1與m2之間的歐式距離d是我們提出使用函數(shù)c=1/(1+d)來(lái)評(píng)估兩個(gè)不確定性模型的接近度.顯然,c的取值范圍是(0,1],兩個(gè)模型之間的距離越小,c值越大.如果兩個(gè)模型完全一樣,則c=1.從表1 第3 列我們可以看到,根據(jù)模型改變的不同,不精確的不確定性模型與精確的模型之間其接近度從0.077 到0.500 之間變化(平均為0.309).另一方面,校準(zhǔn)后的不確定性模型顯示出它們與精確的模型之間的接近度有了顯著的改進(jìn)(如第4 列所示).校準(zhǔn)后模型的接近度從0.552 到0.757之間變化,平均接近度是0.689,提高了122.7%,這表明,校準(zhǔn)后模型的精度已經(jīng)大大提高,且接近精確模型的水平.我們還記錄了適應(yīng)度函數(shù)評(píng)估的迭代次數(shù)和遺傳算法搜索的消耗時(shí)間,分別見(jiàn)表1 第5 列和第6 列.我們利用假設(shè)檢驗(yàn)來(lái)幫助確定校準(zhǔn)的不確定性模型是否足夠精確且具有代表性.如果檢驗(yàn)沒(méi)有通過(guò)的話,則每次多引入10 個(gè)反例到校準(zhǔn)過(guò)程中并重復(fù)校準(zhǔn),而這會(huì)增加搜索消耗的時(shí)間.引入的新反例的實(shí)際概率也需要通過(guò)反例確認(rèn)的實(shí)驗(yàn)統(tǒng)計(jì)獲得.在真實(shí)場(chǎng)景中,我們對(duì)這些反例同樣也執(zhí)行了100 次以獲取其實(shí)際概率.然而,如表1 第7列所示,我們的方法需要的假設(shè)檢驗(yàn)輪數(shù)很少.

Table 1 Calibration results obtained using data from real scenario on the motivating example表1 在驅(qū)動(dòng)案例上使用真實(shí)場(chǎng)景中的數(shù)據(jù)獲得的校準(zhǔn)結(jié)果

在統(tǒng)計(jì)反例的實(shí)際發(fā)生概率時(shí),需要讓系統(tǒng)在反例對(duì)應(yīng)的實(shí)際場(chǎng)景中多次運(yùn)行,觀察反例是否會(huì)觸發(fā)以及觸發(fā)的次數(shù),為了使統(tǒng)計(jì)的概率盡可能地準(zhǔn)確,運(yùn)行的次數(shù)應(yīng)該盡可能地多.但是,由于在實(shí)際場(chǎng)景中反復(fù)確認(rèn)反例的成本較大,因此為了獲取更準(zhǔn)確的統(tǒng)計(jì)概率,我們?cè)谀M場(chǎng)景中也對(duì)反例進(jìn)行了反復(fù)的確認(rèn).在模擬實(shí)驗(yàn)中,我們對(duì)每個(gè)反例執(zhí)行了1 000 次以統(tǒng)計(jì)其實(shí)際概率.另外,模擬實(shí)驗(yàn)還有一個(gè)好處是我們可以改變模擬實(shí)驗(yàn)中精確的不確定性模型,觀察校準(zhǔn)方法對(duì)這些不同模型的校準(zhǔn)是否也有效.表2 報(bào)告了使用從模擬實(shí)驗(yàn)中統(tǒng)計(jì)獲得的反例的實(shí)際概率進(jìn)行校準(zhǔn)后得到的結(jié)果,其中前4 個(gè)模型的變化基于的精確的不確定性模型是:誤差區(qū)間[–6,6]、高斯分布N(0,22).中間4 個(gè)模型的變化基于的精確的不確定性模型是:誤差區(qū)間[–6,6]、高斯分布N(1,22).后4 個(gè)模型的變化基于的精確的不確定性模型是:誤差區(qū)間[–6,6]、高斯分布N(0,32).可以看出,上述真實(shí)場(chǎng)景下的實(shí)驗(yàn)結(jié)論在模擬實(shí)驗(yàn)中也一直保持一致.

需要注意的是,接近度的取值范圍為(0,1],作為一種評(píng)估標(biāo)準(zhǔn),它的值越接近1 就代表校準(zhǔn)的模型與實(shí)際的模型越接近.借助假設(shè)檢驗(yàn)來(lái)幫助我們判斷何時(shí)停止繼續(xù)校準(zhǔn),因此只要通過(guò)檢驗(yàn)就停止校準(zhǔn).這是一種折中的做法,因?yàn)閷?shí)際上我們可以通過(guò)增加反例樣本的數(shù)量不停地重復(fù)校準(zhǔn).實(shí)驗(yàn)中假設(shè)檢驗(yàn)的結(jié)果表明,根據(jù)校準(zhǔn)結(jié)果得出的反例概率與計(jì)算的概率比較接近,所以我們沒(méi)有進(jìn)一步校準(zhǔn),若要獲得更準(zhǔn)確的模型,可以通過(guò)增加校準(zhǔn)時(shí)使用的反例數(shù)量,或者提高假設(shè)檢驗(yàn)的標(biāo)準(zhǔn),來(lái)達(dá)到這一目的,但與此同時(shí),相應(yīng)的校準(zhǔn)成本也會(huì)上升.

Table 2 Calibration results obtained using data from simulation on the motivating example表2 在驅(qū)動(dòng)案例上使用模擬場(chǎng)景中的數(shù)據(jù)獲得的校準(zhǔn)結(jié)果

3.2 校準(zhǔn)算法比較

我們通過(guò)使用遺傳算法來(lái)搜索使適應(yīng)度函數(shù)最小化的不確定性模型參數(shù)的值,以此來(lái)求解校準(zhǔn)問(wèn)題.除遺傳算法外,還可以選擇他算法用于解決這個(gè)問(wèn)題,比如確定的分析方法或其他搜索算法.因此,為了進(jìn)一步評(píng)估方法,我們將遺傳算法與其他方法進(jìn)行了比較.具體地,選擇了另外3 種具有代表性的算法來(lái)求解這個(gè)問(wèn)題:一種基于置信域的分析方法[17]、爬山算法[18]和模擬退火算法[19].

分析的算法是基于常用的置信域方法,在優(yōu)化中常被用于表示使用更簡(jiǎn)單的與模型函數(shù)近似的目標(biāo)函數(shù)的域的子集.然后通過(guò)近似模型函數(shù)和置信域,將原始問(wèn)題轉(zhuǎn)化為更簡(jiǎn)單的置信域子問(wèn)題.我們?cè)趯?shí)驗(yàn)中直接使用MATLAB 優(yōu)化工具箱中的“fminunc”求解器提供的分析方法來(lái)加以實(shí)現(xiàn).同時(shí),我們實(shí)現(xiàn)了爬山算法和模擬退火算法,以搜索不確定性模型參數(shù)的值,從而使適應(yīng)度函數(shù)最小化.所采用的爬山算法是一個(gè)標(biāo)準(zhǔn)的爬山算法,初始搜索點(diǎn)設(shè)定為原始的不精確的不確定性模型的值.對(duì)于模擬退火,除初始搜索點(diǎn)也設(shè)置為原始不精確度不確定性模型的值以外,還有其他幾個(gè)參數(shù),包括初始溫度、降溫速率和迭代次數(shù).參照文獻(xiàn)[19],初始溫度應(yīng)該設(shè)置得足夠高,而降溫速率應(yīng)略小于1.因此,我們嘗試了幾個(gè)不同參數(shù)的值以獲得更好的性能,最終選擇了100作為初始溫度、0.96 作為降溫速率以及20 作為迭代次數(shù).在比較實(shí)驗(yàn)中,只用其他3 種算法代替了我們的遺傳算法.我們的校準(zhǔn)方法的其余部分,包括假設(shè)檢驗(yàn)仍然保持不變.

我們?cè)俅问褂昧蓑?qū)動(dòng)案例作為實(shí)驗(yàn)對(duì)象,精確的不確定性模型是:誤差區(qū)間為[–6,6]、高斯分布為N(0,22).用于校準(zhǔn)的反例的實(shí)際概率來(lái)自于真實(shí)場(chǎng)景.表3 展示了4 種不同算法的校準(zhǔn)結(jié)果.在每一個(gè)含有數(shù)據(jù)的單元格中包含3 個(gè)數(shù)字.第1 個(gè)是校準(zhǔn)后的不確定性模型與精確的模型之間的接近度,第2 個(gè)是求解問(wèn)題的計(jì)算時(shí)間,第3 個(gè)是假設(shè)檢驗(yàn)的輪數(shù).在我們的方法中,當(dāng)校準(zhǔn)的不確定性模型被拒絕后,需要更多的反例作為額外的樣本來(lái)重復(fù)校準(zhǔn)過(guò)程,并且需要準(zhǔn)備反例的計(jì)算概率和實(shí)際概率.然而,重復(fù)校準(zhǔn)過(guò)程將花費(fèi)更多的計(jì)算時(shí)間,而這也包括在總的計(jì)算時(shí)間內(nèi).當(dāng)校準(zhǔn)結(jié)果被假設(shè)檢驗(yàn)拒絕5 次時(shí),我們將終止校準(zhǔn)過(guò)程.表格中我們使用符號(hào)“#”表示沒(méi)有獲得校準(zhǔn)的結(jié)果.

從表中我們可以看到,一般來(lái)說(shuō),基于遺傳算法的方法的求解比其他3 種方法執(zhí)行得更好,即遺傳算法在更短的時(shí)間內(nèi)計(jì)算了更精確的不確定性模型.更具體地說(shuō),由于適應(yīng)度函數(shù)比較復(fù)雜,所以分析算法的能力比較受限,因?yàn)樗枰獔?zhí)行置信域計(jì)算和因式分解.它往往花費(fèi)了更多的計(jì)算時(shí)間.爬山算法在一次迭代搜索中花費(fèi)的時(shí)間較少,但其常常落在局部最優(yōu)中,這使得校準(zhǔn)的不確定性模型容易被假設(shè)檢驗(yàn)多次拒絕,需要重復(fù)校準(zhǔn),最終其總計(jì)算時(shí)間仍多于我們的方法.如實(shí)驗(yàn)結(jié)果所示,爬山算法給出的12 個(gè)校準(zhǔn)不確定性模型中的9 個(gè)被假設(shè)檢驗(yàn)5 次.模擬退火算法比爬山算法略好,但仍遇到類似的問(wèn)題.基于以上討論的實(shí)驗(yàn)結(jié)果可知,我們的基于遺傳算法的校準(zhǔn)方法可以有效地校準(zhǔn)不確定性模型.

Table 3 Comparison of different algorithms in solving calibration problems表3 不同算法求解校準(zhǔn)問(wèn)題的比較

3.3 討 論

本文所提方法的有效性可能會(huì)受到方法中隨機(jī)性的影響.隨機(jī)性的來(lái)源主要是方法中對(duì)于反例實(shí)際概率的統(tǒng)計(jì)以及校準(zhǔn)時(shí)搜索使用的遺傳算法.為了減小它們對(duì)實(shí)驗(yàn)結(jié)論的有效性影響,我們采取了一定的措施,具體而言,對(duì)于實(shí)際概率統(tǒng)計(jì)中存在的隨機(jī)性,為了使統(tǒng)計(jì)的反例的發(fā)生概率與實(shí)際盡可能地相符,我們對(duì)每個(gè)反例在實(shí)際環(huán)境中進(jìn)行了100 次的運(yùn)行以統(tǒng)計(jì)其發(fā)生概率,同時(shí)也在模擬環(huán)境中運(yùn)行了1 000 次.對(duì)于校準(zhǔn)時(shí)搜索使用的遺傳算法自身存在的隨機(jī)性,我們?cè)趯?shí)驗(yàn)階段根據(jù)已有工作的指導(dǎo)經(jīng)驗(yàn)以及多次實(shí)驗(yàn),對(duì)算法的參數(shù)進(jìn)行了審慎的選擇.我們的方法中包含的假設(shè)檢驗(yàn)的部分也能起到降低隨機(jī)性影響的作用.另外,本文處理的不確定性主要是傳感器的感知誤差這類不確定性,對(duì)于其他,例如動(dòng)作執(zhí)行缺陷等不確定性,需要在未來(lái)工作繼續(xù)加以進(jìn)一步研究.

4 相關(guān)工作

由于CPS 的自身特征以及環(huán)境的復(fù)雜性,在CPS 的許多方面都可觀察到不確定性的存在.文獻(xiàn)[2]研究了信息物理系統(tǒng)中不確定性的分類,并按照5C 技術(shù)架構(gòu)[20]對(duì)CPS 中的不確定性進(jìn)行了分類,介紹了架構(gòu)中各層次上可能存在的不確定性.這些不確定性是CPS 中固有存在的,在CPS 的設(shè)計(jì)與實(shí)現(xiàn)過(guò)程中需要對(duì)其進(jìn)行考慮與處理.若未妥當(dāng)處理,不確定性很可能會(huì)影響CPS 的正確運(yùn)行,進(jìn)而導(dǎo)致系統(tǒng)出現(xiàn)各種問(wèn)題.驗(yàn)證是一種有效的質(zhì)量保障方法,已有工作通過(guò)在驗(yàn)證CPS 時(shí)顯式建模不確定性,可以發(fā)現(xiàn)系統(tǒng)中許多潛在的問(wèn)題.但驗(yàn)證時(shí)使用的不確定性模型卻很難在最初就對(duì)其進(jìn)行精確建模,因此本文提出了一種不確定性模型校準(zhǔn)方法.本節(jié)將主要介紹與之相關(guān)的研究工作,具體包括CPS 中不確定性處理以及模型校準(zhǔn)方面的工作.

盡管研究不確定性很重要,但CPS 中不確定性的研究仍處于發(fā)軔之初.為了深入理解CPS 中的不確定性,Zhang 等人[21]通過(guò)回顧各領(lǐng)域不確定性的現(xiàn)有工作,得出了一個(gè)不確定性的概念模型.該概念模型映射到CPS的3 個(gè)邏輯層次:應(yīng)用層、基礎(chǔ)架構(gòu)層和集成層.他們使用UML 類圖以及OCL 約束來(lái)表示該模型.為了確認(rèn)該模型,他們?cè)趦蓚€(gè)不同的工業(yè)案例上對(duì)不確定性進(jìn)行了識(shí)別與描述.為了進(jìn)一步描述CPS 中的不確定性,研究人員提出了多種不確定性建模方法.Cheng 等人[22]提出了一種需求語(yǔ)言RELAX,通過(guò)軟件工程師明確指定系統(tǒng)需求中的不確定性以對(duì)其進(jìn)行處理.該語(yǔ)言采用的是一種附帶布爾表達(dá)式的結(jié)構(gòu)化自然語(yǔ)言形式,使用威脅建模的一種變體來(lái)識(shí)別不確定性,其中威脅是在開(kāi)發(fā)時(shí)帶來(lái)不確定性的各種環(huán)境條件.文獻(xiàn)[23]用SysML 需求圖描述了CPS 中的不確定性,并借此在軟件制品中追蹤不確定性信息.CPS 涉及人、機(jī)、物的融合,為了刻畫(huà)CPS 中人的不確定性行為,文獻(xiàn)[24]提出了一種時(shí)鐘約束規(guī)范語(yǔ)言的概率擴(kuò)展.CPS 中的不確定性可能會(huì)影響系統(tǒng)的運(yùn)行并可能導(dǎo)致嚴(yán)重的后果,發(fā)現(xiàn)問(wèn)題的一種選擇是測(cè)試不確定性對(duì)CPS 的影響.為了支持面向不確定性的CPS 的模型驅(qū)動(dòng)測(cè)試,文獻(xiàn)[25]提出了一個(gè)框架,以創(chuàng)建測(cè)試就緒(test ready)模型,該模型包含CPS 預(yù)期行為以及系統(tǒng)執(zhí)行環(huán)境,并可以用于直接生成測(cè)試用例.驗(yàn)證是發(fā)現(xiàn)不確定性給CPS 帶來(lái)的可能問(wèn)題的另一種途徑.CPS相關(guān)的驗(yàn)證工作較多[5,7,26-28],但只有一些工作[4,9]在驗(yàn)證中明確考慮了不確定性對(duì)系統(tǒng)的影響.我們之前的工作基于ISM 模型對(duì)CPS 進(jìn)行了驗(yàn)證,并在驗(yàn)證中通過(guò)誤差區(qū)間以及概率分布對(duì)不確定性進(jìn)行了明確建模,相比其他不考慮不確定性的驗(yàn)證方法取得了更準(zhǔn)確的驗(yàn)證結(jié)果.但正如之前所述,用于驗(yàn)證的不確定性模型的精確度難以保證.

校準(zhǔn)是一個(gè)通用的術(shù)語(yǔ).在物理學(xué)中,它可以用來(lái)表示評(píng)估和調(diào)整測(cè)量設(shè)備的精度與精度的行為[29],應(yīng)用到不確定性模型的校準(zhǔn)中,一種直接的思路是通過(guò)直接測(cè)量不確定性的參數(shù)來(lái)校準(zhǔn)不確定性模型.與之互補(bǔ),本文采取的校準(zhǔn)思路是通過(guò)觀察不確定性影響的最終結(jié)果來(lái)校準(zhǔn)不確定性模型.通過(guò)直接測(cè)量來(lái)校準(zhǔn)不確定性模型可能導(dǎo)致的一個(gè)問(wèn)題是,通過(guò)直接測(cè)量校準(zhǔn)后的不確定性模型驗(yàn)證得到的反例可能會(huì)與實(shí)際的差距較大.而我們的校準(zhǔn)思路則從結(jié)果出發(fā),是結(jié)果驅(qū)動(dòng)的.我們根據(jù)系統(tǒng)最終的運(yùn)行結(jié)果來(lái)校準(zhǔn)不確定性模型,以使得通過(guò)校準(zhǔn)后的不確定性模型得到的驗(yàn)證結(jié)果更接近實(shí)際,在這個(gè)過(guò)程中,不確定性模型蘊(yùn)含的影響可能不僅僅是自身的.統(tǒng)計(jì)學(xué)中,也可以表示回歸的逆過(guò)程或者統(tǒng)計(jì)分類中用來(lái)確定類成員概率的過(guò)程[30].在我們的問(wèn)題中,它是指調(diào)整不確定性模型的參數(shù),以確保模型盡可能精確地建模出實(shí)際的不確定性.一類與之相關(guān)的工作是模型校準(zhǔn)(model calibration),其目標(biāo)是系統(tǒng)地調(diào)整模型參數(shù),使得輸出能夠更準(zhǔn)確地反映現(xiàn)實(shí)[31].Vanni 等人在文獻(xiàn)[32]中總結(jié)出了模型校準(zhǔn)中的常見(jiàn)過(guò)程:識(shí)別要校準(zhǔn)的輸入,識(shí)別校準(zhǔn)的目標(biāo),度量擬合適應(yīng)度(評(píng)估輸出與觀察數(shù)據(jù)的匹配程度),搜索參數(shù)并接受校準(zhǔn)結(jié)果.該過(guò)程的關(guān)鍵部分是適應(yīng)度的度量和參數(shù)搜索策略.在現(xiàn)有工作中,最常用的適應(yīng)度度量是最小二乘法、加權(quán)最小二乘法與似然函數(shù)[33].本文在校準(zhǔn)過(guò)程中引入了適應(yīng)度函數(shù),使用的度量類似于最小二乘法.在參數(shù)搜索策略方面,有各種各樣的方法來(lái)解決不同類型的搜索問(wèn)題,例如廣義的約減梯度法[34]、模擬退火[19]和遺傳算法[13]等.貝葉斯方法也用于過(guò)模型校準(zhǔn)[35],它定義了模型參數(shù)集的先驗(yàn)分布,并通過(guò)貝葉斯定理更新先前的結(jié)果,以反映在數(shù)據(jù)的似然函數(shù)中給出的附加信息,由此給出后驗(yàn)分布.為了實(shí)現(xiàn)這一點(diǎn),可利用馬爾可夫鏈蒙特卡羅的方法從模型參數(shù)的聯(lián)合后驗(yàn)密度函數(shù)生成樣本[35].

5 總結(jié)

CPS 的使用場(chǎng)景很多都是安全攸關(guān)的,對(duì)系統(tǒng)的質(zhì)量有著較高的要求.而不確定性會(huì)影響到CPS 運(yùn)行的方方面面,若未對(duì)其進(jìn)行妥當(dāng)處理很可能會(huì)對(duì)系統(tǒng)質(zhì)量產(chǎn)生極大的負(fù)面影響.驗(yàn)證可以用于研究不確定性對(duì)CPS質(zhì)量的影響,及早發(fā)現(xiàn)系統(tǒng)中的問(wèn)題.已用工作在這一問(wèn)題上取得了一些進(jìn)展,驗(yàn)證CPS 時(shí)通過(guò)建模不確定性明確考慮了不確定性對(duì)系統(tǒng)的影響,相比傳統(tǒng)方法取得了更為準(zhǔn)確的驗(yàn)證結(jié)果.然而,由于測(cè)量過(guò)程中不可控的噪聲和數(shù)據(jù)樣本數(shù)量不足,很難在最初就精確地建模系統(tǒng)與環(huán)境之間交互的不確定性.本文提出了一種校準(zhǔn)CPS中不精確的不確定性模型的方法,該方法利用當(dāng)不確定性模型精確時(shí)反例的計(jì)算概率應(yīng)與實(shí)驗(yàn)中統(tǒng)計(jì)獲得的反例的實(shí)際發(fā)生概率接近這一觀察,將不確定性模型的校準(zhǔn)問(wèn)題轉(zhuǎn)化為一個(gè)搜索問(wèn)題.之后,利用遺傳算法來(lái)求解該問(wèn)題,找到使得反例的計(jì)算概率與實(shí)際概率差異最小的精確的不確定性模型.同時(shí),借助假設(shè)檢驗(yàn)判斷校準(zhǔn)后的不確定性模型是否足夠精確且沒(méi)有過(guò)于匹配于選定的反例.基于實(shí)際案例上的實(shí)驗(yàn)結(jié)果表明,我們的方法能夠有效地校準(zhǔn)不精確的不確定性模型.