基于反例確認的CPS 不確定性模型校準*

楊文華 ,周 宇 ,黃志球

1(南京航空航天大學 計算機科學與技術學院,江蘇 南京 211106)

2(高安全系統的軟件開發與驗證技術工信部重點實驗室(南京航空航天大學),江蘇 南京 211106)

3(軟件新技術與產業化協同創新中心,江蘇 南京 210093)

信息物理系統(cyber-physical system,簡稱CPS)涵蓋了人、機、物的融合,它借助技術手段將人的控制延伸至信息與物理世界.CPS 涉及環境感知、嵌入式計算、網絡通信和控制等系統工程,其目標是使物理系統具有計算、通信、精確控制、遠程協作和自治能力.它注重計算資源與物理資源的緊密結合與協調,其應用領域非常廣泛,包括工業控制、智能制造、智能交通、遠程醫療、智能電網、航空航天等領域[1].研究CPS 對于相關領域軟件的發展具有十分重要的意義.

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

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

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

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

本文第1 節介紹我們所使用的驅動案例,一個自動避障與搜索小車系統.第2 節詳細介紹我們提出的不確定性模型校準方法.第3 節展示校準方法在驅動案例上的實驗結果以及分析.第4 節介紹目前對CPS 中不確定性進行處理的相關工作.最后第5 節是總結.

1 驅動案例

自動小車是一類典型的信息物理系統[1].圖1 展示的是一個自動小車系統的運行場景.小車的主要功能是探索整個區域并避免碰撞到任何障礙物.小車可以在方格內執行相應動作,移動到東南西北4 個方位的其他方格內.小車車身四周配備了傳感器,可以感知四周障礙物的距離.為了確認小車對區域探索是否廣泛,區域內設置了一些檢查點,小車巡視到檢查點時會收到相應信號.自動小車系統會基于感知到的距離來決定小車的探索動作并躲避障礙物.如果小車撞到障礙物,則認為自動小車系統失效,或者小車的運行步數超出了一個閾值卻仍未巡視到所有檢查點,這種現象也認為是失效.

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

Fig.1 The running scenario of the robot-car system圖1 自動小車系統運行場景

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

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

2 基于反例確認的模型校準方法

為了獲取更準確的驗證結果,我們的已有工作在驗證CPS 時考慮了系統中的不確定性[9].相較其他驗證方法,該方法可以檢測到許多被其他方法忽略的真實反例.而該驗證方法的一個重要輸入是不確定性模型.建模不確定性時使用的是物理學中常用的誤差區間與分布.以傳感器感知的不確定性為例,在感知時傳感器不可避免地存在誤差,運行時我們卻無法確認具體的誤差值是多少.但這個誤差一般存在一個大概的范圍且常常可以用某種分布對其進行刻畫.

然而,由于測量過程中不可控制的噪聲和數據樣本數量存在一定的局限性,很難在最初就精確而完整地建模系統中的不確定性[10].從而使得用于驗證的不確定性模型不精確.這里,不確定性模型具體代表建模不確定性時所用的誤差區間與相關分布的一些參數(如高斯分布的均值和方差).而這些不精確的模型會導致驗證結果偏離現實:不太重要的反例可能被錯誤地突出顯示(如本來低概率的反例變成了高概率),或者更糟的是,還有可能會報告一些錯誤的反例(如現實中不會發生).具體的表現形式可以是,所報告的反例的概率與實際中統計的反例發生的概率相差甚遠,因為不確定性模型是計算反例概率的關鍵輸入.不精確的不確定性模型會導致所報告的反例的計算概率與真實場景中統計的實際概率之間出現不一致.基于這一關鍵觀察,我們提出通過反例確認,比較反例計算概率和執行中統計的實際概率之間的差異來發現不精確的不確定性模型,并基于反例確認的結果來進行模型的校準.接下來,我們將詳細介紹所提出的不確定性模型校準方法.

2.1 方法概述

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

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

2.2 反例確認

不精確的不確定性模型會導致驗證結果偏離現實.反之,通過對驗證結果進行確認,可以發現用于驗證的不確定性模型是否精確.換言之,我們可以讓系統在反例對應的實際場景下運行,統計反例是否會觸發以及觸發的頻率.根據這些信息,可以獲得反例的實際發生概率.然后將反例的計算概率與實際概率進行比較,就能識別出不確定性模型是否精確.

已有工作[4]通過遍歷CPS 對應的ISM 模型的每條候選路徑來收集系統的行為,并獲取路徑的路徑條件,其中與環境相關的變量使用了誤差區間來引入不確定性.失效條件描述了系統的故障,通過把失效條件與路徑條件合取再使用SMT 求解器對條件進行求解可以得到驗證結果.如果條件滿足的話,則意味著系統會失效,而求解器返回的解與路徑一起組成一個反例.反例描述了系統的執行軌跡,其中包含失效條件與路徑條件中變量的取值,這些值可以對應到導致系統失效的環境輸入.

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

Fig.3 An example of the environment construction for a counter example圖3 反例對應的環境構造示例

反例中包含的信息十分豐富,根據反例如何構造實際場景亦很直觀,因此這里不再贅述.而反例確認就是讓系統在該反例對應的實際場景下來運行,觀察反例能否觸發.在觀察的過程中,我們還可以記錄系統運行的次數以及每一次的運行情況,從而可以統計出反例的實際概率.若通過比較反例計算概率以及實際概率發現兩者之間的差異較大,則可以安全地判斷出不確定性模型不夠精確,需要進一步校準.

2.3 校準問題求解

為了校準不精確的不確定性模型,我們提出將校準問題轉化為一個搜索問題.給定一組具有實際概率和計算概率的反例,搜索以已有驗證中使用的不確定性模型作為起始點,搜索能夠最小化適應度函數的不確定性模型.而適應度函數是關于反例的實際概率和計算概率之間的差異.更具體地,不確定性模型是使用誤差區間與分布進行建模的,而這些又表征為具體的參數,例如高斯分布的均值和方差.因此,搜索問題的本質就是找到最小化適應度函數的不確定性模型參數的值.下面,我們詳細介紹適應度函數的定義以及所使用的搜索算法.

2.3.1 適應度函數的定義

適應度函數描述的是搜索問題的目標,并通常根據相關的度量標準或屬性而加以定義.如前所述,校準需要首先發現所選反例的計算概率和實際概率之間的不一致性.我們通過計算這兩種概率之間的差異,并使用其絕對值的總和除以反例的個數來描述不一致性的程度.由于我們的目標是找到適當的誤差區間和分布的參數值,使得所選擇的反例的計算概率與實際概率之間的不一致最小化,所以我們直接將上述計算不一致性的函數作為適應度函數.為了獲得反例的實際概率,我們讓系統在反例相應的環境中運行固定次數,并統計反例的觸發次數.那么觸發次數與總次數的比值就是反例實際的概率.由于反例的個數可能很多,所以獲取所有反例的實際概率可能是非常耗時與不實際的,所以我們只選擇了一部分反例來作為樣本.選擇反例的策略可以有很多,但是我們建議先選擇具有高概率的反例,這樣可以加快校準過程.

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

2.3.2 搜索算法

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

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

算法1.基于遺傳算法的校準.

輸入:不確定性模型U,選擇的反例集合Θ,最大迭代次數n,閾值?(用于衡量兩次連續評估值之間的差異);

輸出:校準后的不確定性模型s.

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

在迭代過程中,有幾個關鍵的操作:選擇(Line 9)、交叉(Line 10)和變異(Line 11).下面我們詳細加以介紹.

· 選擇.它根據評估值為子代個體選擇父代個體.對于每一個個體i,其評估值evali就是適應度函數以個體i為不確定性模型的函數值fit.我們采用了一種標準的選擇方法(輪盤賭方法),其中,個體i被選擇的概率是evali是個體i的評估值,m是個體的總個數.被選擇的個體都在選擇池中.

· 交叉.它通過交叉兩個父代個體來為新種群形成兩個新的子代個體.為了選擇交叉的父代,給定一個交叉概率pc,我們隨機地從選擇池中選擇pm×m/2 個父代.在具體的交叉操作中,單點交叉策略被應用.然后,選擇池中父代被其子代所代替.

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

遺傳算法的參數(例如,交叉概率pc與變異概率pm)設置是問題依賴的.一般來說,增大變異概率可能會增加遺傳的多樣性,但會導致搜索過于分散在解空間上,從而增大了交叉概率,可導致算法在解空間上相對集中的區域進行搜索.我們也可以根據實驗的反饋來調整參數.同時,現有的文獻總結了許多有價值的經驗,供我們處理問題時參考[15].根據建議,從[0.4,0.9]與[0.0001,0.1]中分別選擇交叉概率和變異概率的值是安全的.算法獲得的解包含了表示校準的不確定性模型的參數變量的值.

2.4 假設檢驗

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

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

3 實驗評估

本節評估校準方法的有效性,具體考慮以下兩個研究問題.

研究問題1:我們的方法能不能有效地校準不確定性模型?

研究問題2:與其他算法相比,我們校準中使用的遺傳算法表現如何?

在評估中我們使用第1 節介紹的驅動案例作為實驗對象.該CPS 使用ISM 進行建模,詳細的ISM 模型取自文獻[4,9].借助已有工作中的驗證方法,可以對該自動小車系統進行驗證,獲取系統的反例并計算出這些反例的概率.

3.1 校準的有效性

本實驗評估的是采用我們的方法校準CPS 中不精確的不確定性模型的有效性.為了評估校準的有效性,我們首先需要得到不精確的不確定性模型,進行校準后再與精確的模型進行對比.實驗中,校準的不精確的不確定性模型是在已有的一個精確的不確定性模型上改變得到的.在我們已有的工作[4]中,通過大量針對自動小車系統的實驗可以發現,使用的一個已有的不確定性模型可以準確地估算反例的概率.因此可以認為這個已有的不確定性模型是足夠精確的,我們也用其作為實驗中的精確的不確定性模型的基準.不精確的不確定性模型是在這個模型(誤差區間為[–6,6],分布為高斯分布N(0,22))的變化上得到的.

具體來說,我們識別了3 個控制變量:誤差區間以及分布的均值和方差.這些變量的變化是以每次改變一個變量的受控方式進行的,我們對這些變量分別單獨增大或減小了±1 與±2,即每個變量都進行了減小1 或2,增大1 或2 共4 種變化.通過一系列實驗來檢查我們的方法是否可以成功地校準那些不精確的不確定性模型.基于自動小車系統的反例來校準不精確的不確定性模型,自動小車系統的每個反例都具有計算概率和實際概率.計算概率是用不精確的不確定性模型計算得到的,實際概率是從實驗中統計獲得的.然后,將這些不精確的不確定性模型與反例一起傳遞給我們的校準方法進行校準.

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

Table 1 Calibration results obtained using data from real scenario on the motivating example表1 在驅動案例上使用真實場景中的數據獲得的校準結果

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

需要注意的是,接近度的取值范圍為(0,1],作為一種評估標準,它的值越接近1 就代表校準的模型與實際的模型越接近.借助假設檢驗來幫助我們判斷何時停止繼續校準,因此只要通過檢驗就停止校準.這是一種折中的做法,因為實際上我們可以通過增加反例樣本的數量不停地重復校準.實驗中假設檢驗的結果表明,根據校準結果得出的反例概率與計算的概率比較接近,所以我們沒有進一步校準,若要獲得更準確的模型,可以通過增加校準時使用的反例數量,或者提高假設檢驗的標準,來達到這一目的,但與此同時,相應的校準成本也會上升.

Table 2 Calibration results obtained using data from simulation on the motivating example表2 在驅動案例上使用模擬場景中的數據獲得的校準結果

3.2 校準算法比較

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

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

我們再次使用了驅動案例作為實驗對象,精確的不確定性模型是:誤差區間為[–6,6]、高斯分布為N(0,22).用于校準的反例的實際概率來自于真實場景.表3 展示了4 種不同算法的校準結果.在每一個含有數據的單元格中包含3 個數字.第1 個是校準后的不確定性模型與精確的模型之間的接近度,第2 個是求解問題的計算時間,第3 個是假設檢驗的輪數.在我們的方法中,當校準的不確定性模型被拒絕后,需要更多的反例作為額外的樣本來重復校準過程,并且需要準備反例的計算概率和實際概率.然而,重復校準過程將花費更多的計算時間,而這也包括在總的計算時間內.當校準結果被假設檢驗拒絕5 次時,我們將終止校準過程.表格中我們使用符號“#”表示沒有獲得校準的結果.

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

Table 3 Comparison of different algorithms in solving calibration problems表3 不同算法求解校準問題的比較

3.3 討 論

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

4 相關工作

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

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

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

5 總結

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