狀態(tài)不可觀測的信息物理融合系統(tǒng)運行時驗證

狀態(tài)不可觀測的信息物理融合系統(tǒng)運行時驗證房丙午;黃志球;王勇;李勇【摘要】確保信息物理融合系統(tǒng)(Cyber-PhysicalSystem,CPS)運行時行為正確性是至關(guān)重要的,尤其在航空航天、汽車、核電和醫(yī)療等安全攸關(guān)領(lǐng)域.本文針對具有隨機行為且狀態(tài)不可觀測的CPS,提出一種基于隱馬爾科夫模型的運行時安全性驗證方法?首先構(gòu)造狀態(tài)不可觀測的CPS運行時安全性驗證框架,該框架通過隱馬爾科夫模型表示系統(tǒng),使用確定性有限自動機規(guī)約系統(tǒng)安全屬性的否定,兩者的乘積自動機作為運行時監(jiān)控器，從而將CPS運行時安全性驗證問題約簡到監(jiān)控器上的概率推斷問題?然后，提出一種增量迭代安全性驗證算法以及反例生成算法?實驗結(jié)果表明本文算法和粒子濾波算法相比預測錯誤率下降了近20％,并且當系統(tǒng)違背安全屬性時,本文的方法能給出反例.期刊名稱】《電子學報》年(卷),期】2018(046)012【總頁數(shù)】8頁(P2824-2831)【關(guān)鍵詞】信息物理融合系統(tǒng);運行時驗證;隱馬爾科夫模型;確定性有限自動機;安全性;反例【作者】房丙午;黃志球;王勇;李勇【作者單位】南京航空航天大學計算機科學與技術(shù)學院,江蘇南京210016;安徽財貿(mào)職業(yè)學院云桂信息學院,安徽合肥230061;南京航空航天大學計算機科學與技術(shù)學院,江蘇南京210016;南京航空航天大學計算機科學與技術(shù)學院,江蘇南京210016;南京航空航天大學計算機科學與技術(shù)學院,江蘇南京210016正文語種】中文【中圖分類】TP311引言CPS在航空航天、汽車、核電和醫(yī)療等安全攸關(guān)的領(lǐng)域有著廣闊的應(yīng)用前景［1,2］，因此，確保CPS運行時行為正確性是至關(guān)重要的?運行時驗證通過監(jiān)控系統(tǒng)運行時的執(zhí)行軌跡來驗證系統(tǒng)是否滿足屬性規(guī)約［3］,是保證CPS運行時行為正確性的有效方法?文獻［3~5］針對實時性要求較高的CPS，驗證與時間相關(guān)的功能正確性?文獻［6］針對CPS運行時失效行為進行監(jiān)控?在CPS運行時安全性驗證方面，文獻［7］給出在不可靠的網(wǎng)絡(luò)通信下，對CPS的安全屬性不變式進行運行時驗證，不變式是一類基于狀態(tài)的使用謂詞邏輯描述的安全屬性，該方法不能驗證無限狀態(tài)時序序列的安全屬性?文獻［8］使用混成自動機建模自適應(yīng)巡航控制系統(tǒng)，使用CHARON語言規(guī)約安全屬性，驗證了自適應(yīng)巡航控制系統(tǒng)運行時安全性.雖然研究人員提出了多種CPS運行時驗證的方法，但目前的研究存在以下不足:(1)現(xiàn)有的研究都假設(shè)系統(tǒng)運行時的狀態(tài)可以直接觀測的，實際上大多數(shù)復雜的CPS在運行時其狀態(tài)是不可觀測的［9,10］.(2)在運行時安全性驗證中，當系統(tǒng)違背安全屬性時，而沒有給出相應(yīng)的反例［11］.針對上述不足，本文提出了狀態(tài)不可觀測的具有隨機行為的CPS運行時安全性驗證方法?由于系統(tǒng)狀態(tài)不可觀測，因此，采用隱馬爾科夫模型(HiddenMarkovModel,HMM)來建模系統(tǒng)?使用確定性有限自動機(DeterministicFiniteAutomaton,DFA)規(guī)約安全屬性的否定，安全屬性監(jiān)控器由HMM和DFA的乘積自動機表示，從而將狀態(tài)不可觀測的CPS運行時安全性驗證問題約簡到監(jiān)控器上的概率推斷問題.運行時驗證框架本文的驗證問題可描述為：給定系統(tǒng)狀態(tài)轉(zhuǎn)換模型TS，系統(tǒng)安全屬性申safe以及系統(tǒng)運行時的觀測序列o1,...,ot，目標是(1)計算在t時刻系統(tǒng)滿足安全屬性的概率Prt(TS申safe|o1,...,ot;TS),(2)當系統(tǒng)違背安全屬性時，求解系統(tǒng)最大可能的執(zhí)行路徑作為系統(tǒng)違背安全屬性的反例.針對該問題，圖1給出了本文驗證方法的框圖1中，虛線框中是運行時驗證的監(jiān)控器單元，監(jiān)控器由系統(tǒng)模型和屬性自動機的乘積來表示，其中，系統(tǒng)模型由HMM表示，屬性自動機由DFA表示?監(jiān)控器的輸入是運行時系統(tǒng)的觀測序列和系統(tǒng)安全性的閾值Pth，監(jiān)控器輸出是當前系統(tǒng)滿足安全性的概率，當系統(tǒng)安全性概率低于閾值時，輸出反例.系統(tǒng)模型的構(gòu)造可以來自于系統(tǒng)設(shè)計模型［9］，或通過領(lǐng)域?qū)＜抑付ㄏ到y(tǒng)狀態(tài)以及狀態(tài)的觀測值，然后模擬系統(tǒng)運行獲取系統(tǒng)觀測數(shù)據(jù)并學習一個系統(tǒng)模型［10］.系統(tǒng)的安全屬性采用線性時序邏輯描述，使用DFA來識別安全屬性的否定也就是識別系統(tǒng)運行中違反安全性的有限前綴.相關(guān)定義與監(jiān)控器模型3.1相關(guān)定義本文采用HMM建模系統(tǒng)，采用DFA描述系統(tǒng)安全屬性，下面給出相關(guān)的定義.定義1-個DFA是如下形式的五元組A=(QZ、q0,F).其中，Q是有限的，非空的狀態(tài)集合，1是輸入字母表,Z=2AP,AP為原子命題集合，S:QxZ-Q是一個狀態(tài)轉(zhuǎn)換函數(shù)，q0EQ是一個初始狀態(tài)，F(xiàn)Q是接受狀態(tài)的集合.如果在A中Vq^Q,VBW2AP都有Q(q,B)|=1,那么A是一個完全的DFA.—個完全的DFA對于每個輸入字oe(2AP)w都存在一個唯一的運行與之對應(yīng).定義2—個離散時間馬爾科夫鏈(Discrete-TimeMarkovChain,DTMC)是一個四元組C=(S,P,iinit,L)?其中：S表示可數(shù)非空的狀態(tài)集合，P:SxS-[0,1]是狀態(tài)轉(zhuǎn)換概率分布函數(shù)，對每一個狀態(tài)⑶iinit:S-[0,1]是初始狀態(tài)概率分布函數(shù)，(4)L:S-2AP是標簽函數(shù).定義3—個HMM是一個三元組H=(C,O,p)?其中：C是一個DTMC,O是系統(tǒng)可觀測符號的有限集合，即系統(tǒng)模型輸出的有限集合，p:Sx2O-[0,1]是一個觀測符號概率分布函數(shù)，對于VM(s,o)或ps(o)表示系統(tǒng)在狀態(tài)s時產(chǎn)生觀測o的概率，相同的觀測可能由幾個不同的系統(tǒng)狀態(tài)產(chǎn)生，因此，在已知目前觀測的情況下系統(tǒng)的狀態(tài)是不確定的.3.2監(jiān)控器模型本文將安全屬性監(jiān)控器定義為一個A和H的乘積自動機，系統(tǒng)安全屬性是基于可觀測符號描述，因此，A的輸入字母表》匸2O.定義4安全屬性監(jiān)控器定義為一個A和H的乘積自動機M=A其中，S'=SxQ,監(jiān)控器狀態(tài)集合；P'(〈s,q〉,〈s：q'〉)二表示狀態(tài)轉(zhuǎn)換概率分布，其中,T=O(s,)n8-1(q,q,),O(s,)c20表示在狀態(tài)s'觀測字母的集合,6-1(q,q,)c丄表示A中從狀態(tài)q到q‘的輸入字母的集合；F=SxF,監(jiān)控器接受狀態(tài)集合；監(jiān)控器初始狀態(tài)概率分布，其中,T=0(s)n8-1(q0,q)；⑸『(〈s,q〉，o)=ps(o),owT,表示狀態(tài)〈s,q〉觀測符號概率分布.根據(jù)定義可知，監(jiān)控器M本質(zhì)上是一個含有接受狀態(tài)集的HMM,并且M的狀態(tài)集S'=SxQ中存在一些從初始狀態(tài)不可達的狀態(tài)以及與監(jiān)控屬性無關(guān)的狀態(tài)，因此，要從M中移除這些狀態(tài)?采用寬度優(yōu)先算法來構(gòu)造M，首先構(gòu)造M的所有初始狀態(tài)?然后，從初始狀態(tài)出發(fā)，采用寬度優(yōu)先搜索算法來生成M的狀態(tài)?根據(jù)定義4，監(jiān)控器構(gòu)造時間復雜度為:O(|O|x(|S|x|O|)2),其中，|0|表示系統(tǒng)可觀測符號集合的勢.安全性驗證和反例生成算法監(jiān)控器接受當前的系統(tǒng)觀測，更新信念狀態(tài)并計算在已知整個有窮觀測序列下的系統(tǒng)安全性概率?基于監(jiān)控器模型，本節(jié)提出一種增量迭代安全性驗證算法(IncrementalIterativeVerification,IIV)算法以及系統(tǒng)違背安全性需求時的反例生成算法.4.1安全性驗證算法定義5信念狀態(tài)(beliefstate)是指在時刻t，已知系統(tǒng)的觀測序列o1,o2,...,ot,監(jiān)控器M處在狀態(tài)s的概率?形式化表示為：bt(s)二Pr(s|o1,o2,...,ot;M),由于觀測值是從系統(tǒng)的不同狀態(tài)發(fā)出的，因此無法知道系統(tǒng)目前所處的準確狀態(tài)也就是M所處的狀態(tài)，但是根據(jù)系統(tǒng)的歷史觀測，能夠計算出系統(tǒng)的信念狀態(tài)?由定義5可知，系統(tǒng)的信念狀態(tài)也可由HMM的前向或后向概率表示［12］，但前(后)向算法需要處理從初始觀測開始到當前時刻的觀測序列，當一個新的觀測值到達時，為了更新系統(tǒng)信念狀態(tài)，前(后)向算法每次都要處理從當前觀測之前的整個觀測序列?隨著系統(tǒng)觀測序列的增長，前(后)向算法消耗的內(nèi)存和計算時間也將增長?為了能夠快速地反應(yīng)系統(tǒng)信念狀態(tài)的變化，本節(jié)提出IIV算法，一旦收到一個新的觀測值，算法立即更新系統(tǒng)信念狀態(tài)，該算法以在線遞推方式計算系統(tǒng)信念狀態(tài)，在t=1時，系統(tǒng)信念狀態(tài)b1(s)取決于初始狀態(tài)分布和初始觀測值o1根據(jù)HMM的齊次馬爾科夫假設(shè)可知，系統(tǒng)在t時刻的信念狀態(tài)bt(s)只依賴于bt-1(s)時刻的狀態(tài)和當前的觀測ot.引理1給出了bt(s)和bt-1(s)之間的關(guān)系.引理1給定系統(tǒng)的歷史觀測序列o1,o2,...,ot，M的信念狀態(tài)更新函數(shù)bt(s)可表示為如下遞推公式：其中，證明根據(jù)信念狀態(tài)的定義和貝葉斯定理可得t=1時信念狀態(tài)：b1(s)假設(shè)在t>1時，已知bt-1(s)和當前的觀測ot，則系統(tǒng)在t時刻的信念狀態(tài)：bt(s)=Pr(s|o1,.,ot)(3)其中，Pr(s,ot|o1,.,ot-1)Pr(s,ot|s：o1,...,ot-1)(4)(5)將式(4)和式(5)的結(jié)果代入式(3)即可得出式(2).定理1令申safe是系統(tǒng)的安全屬性，A是一個接受申safe所有壞前綴集合的DFA,H是表示系統(tǒng)模型的HMM,監(jiān)控器M=AH,o1,o2,...,ot,是系統(tǒng)運行時的觀測序列?那么在t時刻系統(tǒng)安全性的概率：Prt(H甲safe|o1,...,ot)二Prt(M甲safe|o1,...,ot)證明(1)由于A是完全確定性自動機，所以A不會影響監(jiān)控器M中的概率計算?另外，如果H中某一狀態(tài)不包含在M的組合狀態(tài)中，則該狀態(tài)與監(jiān)控屬性無關(guān)，也不會影響監(jiān)控器M中的概率計算?所以，Prt(H甲safe|o1,...,ot)二Prt(M甲safe|o1,...,ot).(2)首先，自動機A接受安全屬性的否定，也就是接受的是壞前綴，所以M中的接收狀態(tài)集F是系統(tǒng)的不安全狀態(tài)?其次，在M構(gòu)造過程中刪除了從初始狀態(tài)不可達狀態(tài)以及與監(jiān)控屬性無關(guān)的狀態(tài)，而這些狀態(tài)相對于申safe來說是安全狀態(tài)，因此t時刻系統(tǒng)安全性的概率Prt(M根據(jù)引理1和定理1,算法1給出根據(jù)系統(tǒng)的當前觀測ot計算系統(tǒng)安全性概率的算法.在算法1中，語句1~9是根據(jù)式(1)進行信念狀態(tài)初始化，僅在算法啟動時執(zhí)行—次?語句10~15是計算式(2)的分子部分和分母zt,語句16~18是計算t時刻的信念狀態(tài)，語句20返回系統(tǒng)安全性概率.從算法1中可以看出語句12執(zhí)行次數(shù)最多,可以通過分析語句12最大執(zhí)行次數(shù)來分析算法的最壞時間復雜度?由語句10~15可知，語句12的執(zhí)行次數(shù)為|S[2,因此，算法1的時間復雜度為O(|S[2).4.2反例生成算法在隨機模型檢測中,當系統(tǒng)屬性被違背時,對反例的產(chǎn)生方法進行了大量的研究[11].在運行驗證中，系統(tǒng)當前執(zhí)行路徑只有一條，當系統(tǒng)違背安全屬性時，該路徑就是當前運行的一個反例.在狀態(tài)不可觀測的情況下，通過觀測序列推斷系統(tǒng)最大可能的執(zhí)行路徑，因此，當系統(tǒng)違背安全屬性時，本文將當前觀測序列下的最大可能執(zhí)行路徑作為系統(tǒng)運行時的一個反例.定義6給出了最大可能執(zhí)行路徑的定義.定義6已知系統(tǒng)觀測序列o1,o2,...,oT,當系統(tǒng)違背安全屬性時，監(jiān)控器M的最大可能執(zhí)行路徑其中，siwS：i=12...,T.由定義6可知，求解M中長度為T的最大可能執(zhí)行路徑的時間復雜度為O(|S［T),顯然不能滿足運行時驗證需求.對于該問題可以采樣隨機優(yōu)化算法近似求解［13］，本文采用動態(tài)規(guī)劃算法來求解，下面的引理給出了系統(tǒng)反例的生成方法.引理2已知監(jiān)控器M和系統(tǒng)運行時觀測序列o1,o2,...,oT,⑴求解最大可能執(zhí)行路徑等價于求解定義在時刻t(tvT)狀態(tài)為s的所有單個路徑中概率最大值則在時刻t+1狀態(tài)為s的所有單個路徑中概率最大值證明(1)由貝葉斯定理可知，由于是規(guī)范化因子(常數(shù))，所以，Pr(s1,s2,...,sT|o1,o2,...,oT)yPr(s1,s2,...,sT,o1,o2,...,oT)由此可得引理2中⑴成立.(2)根據(jù)定義，根據(jù)貝葉斯定理，Pr(s1,s2,.,st,s,o1,o2,.,ot+1)=Pr(s1,s2,.,st,o1,o2,.,ot)Pr(s|st)Pr(ot+1|s).對上式求最大值并根據(jù)動態(tài)規(guī)劃原理可得：Pr(ot+1|s)根據(jù)引理2,算法2給出了系統(tǒng)反例生成算法，算法2中的Et(s)表示在時刻t狀態(tài)為s的所有單個路徑中概率最大的路徑的第t-1個狀態(tài)，將M的最大可能執(zhí)行路徑投影到系統(tǒng)模型H上從而獲得系統(tǒng)的最大可能執(zhí)行路徑.語句2~5根據(jù)當前的信念狀態(tài)初始化yKs)和EKs),語句6~11遞推計算在t時刻到達狀態(tài)s最大可能路徑的概率以及概率最大路徑的前驅(qū)，語句12獲取最大可能路徑的終點，語句13~15回溯獲取最大可能執(zhí)行路徑，語句16返回系統(tǒng)最大可能執(zhí)行路徑?從算法2中可以看出語句8執(zhí)行次數(shù)最多，最大執(zhí)行次數(shù)是:Tx$|2,因此，算法2的時間復雜度為O(Tx|S[2).算法2生成的反例長度取決于輸入觀測序列長度T.案例分析與實驗本節(jié)通過汽車安全車道保持系統(tǒng)[14](SAFELANE)來驗證本文方法的有效性和計算效率?汽車控制系統(tǒng)是一個安全攸關(guān)的CPS，其中SAFELANE是商用和家用汽車主動安全系統(tǒng)的重要組成部分，SAFELANE是防止駕駛員疏忽或疲勞而造成的無意識的車道偏離.當系統(tǒng)工作時，一旦探測到意外的車道偏離時，系統(tǒng)向駕駛員發(fā)出警告或主動校正車道使其恢復到正常狀態(tài)，為了能夠執(zhí)行車道校正，系統(tǒng)必須獲得駕駛車輛的權(quán)限.系統(tǒng)能夠被駕駛員的操作行為覆蓋(如駕駛員轉(zhuǎn)向操作)或通過人機交互接口關(guān)閉.SAFELANE由視覺傳感、決策控制、執(zhí)行、轉(zhuǎn)向控制、速度控制等子系統(tǒng)組成，其中，決策控制子系統(tǒng)采用冗余計算方式，主系統(tǒng)和熱備份系統(tǒng)并行計算，如果兩者的計算結(jié)果不一致，則系統(tǒng)進入故障狀態(tài).實驗設(shè)置針對SAFELANE主動控制模式進行安全屬性驗證，圖2給出了該模式對應(yīng)的HMM,其中，s1表示系統(tǒng)處在空閑狀態(tài)，s2表示系統(tǒng)處在決策狀態(tài)，s3表示系統(tǒng)處在車道校正狀態(tài)，s4表示主系統(tǒng)和熱備份系統(tǒng)計算結(jié)果不一致狀態(tài)，s5表示系統(tǒng)處在未知故障狀態(tài)?系統(tǒng)可觀測符號，IL(InLane)表示汽車在車道上，ULD(UnintentionalLaneDeparture)表示無意識的車道偏離，RC(RequestingControl)表示請求控制，CRG(ControlRequestingGranted)表示控制請求已授權(quán)，AF(ActuatorFail)表示執(zhí)行子系統(tǒng)失效，表1為模型參數(shù)?待驗證的系統(tǒng)安全屬性為：“如果執(zhí)行子系統(tǒng)失效,SAFELANE將不能獲取車輛的控制權(quán)”其LTL公式為：HAF-gCRG)).將該LTL公式轉(zhuǎn)換為成DFA，如圖3所示，圖中的雙圓圈表示DFA的接受狀態(tài)，DFA輸入字母表》={{},{AF},{CRG},{AF,CRG}}.實驗運行在intelcorei5雙核2.4GHzCPU,8GB內(nèi)存，64位WinlO操作系統(tǒng)上.通過HMMMATLAB工具箱模擬系統(tǒng)運行?為了評估本文IIV算法的計算性能，本節(jié)將IIV算法和粒子濾波算法(ParticleFilter,PF)[15]進行比較.PF算法的粒子數(shù)為500.表1系統(tǒng)可觀測變量及參數(shù)值設(shè)置系統(tǒng)狀態(tài)初始概率分布系統(tǒng)觀測變量及概率分布ILULDRCCRGAFs11.00.00.0s20.00.00.0s30.00.00.10.00.90.0s40.00.00.00.00.10.9s50.00.00.00.00.01.0安全屬性驗證模擬系統(tǒng)運行100次，每次產(chǎn)生觀測序列的長度為50，系統(tǒng)安全性概率閾值為0.95，如果當前系統(tǒng)安全性概率低于閾值，監(jiān)控器根據(jù)當前的監(jiān)控情況產(chǎn)生長度為10的反例并終止本次運行.在100次運行中，共計探測到4次系統(tǒng)安全性概率低于給定的閾值，表2列出了當系統(tǒng)安全性概率低于閾值時的觀測序列及產(chǎn)生的反例.表2系統(tǒng)安全性概率及生成的反例序號輸入的觀測序列安全性概率最大可能執(zhí)行路徑是否反例1IL,RC,CRG,IL,RC,CRG,IL,RC,CRG,AF0.9009s1,s2,s3,s1,s2,s3,s1,s2,s3,s4否2IL,RC,CRG,IL,CRG,CRG,IL,RC,AF,CRG0.2447s1,s2,s3,s1,s2,s3,s1,s2,s4,s3是3ULD,RC,CRG,IL,RC,CRG,ULD,RC,AF,AF0.9101s1,s2,s3,s1,s2,s3,s1,s2,s4,s4否4RC,CRG,IL,RC,CRG,IL,RC,AF,ULD,CRG0.1870s2,s3,s1,s2,s3,s1,s2,s4,s4,s2是從表2中可以看出，第一行和第三行是請求控制被授權(quán)后，系統(tǒng)執(zhí)行車道校正時,執(zhí)行機構(gòu)失效了，系統(tǒng)安全性概率降低了，但系統(tǒng)沒有違背安全屬性,此時產(chǎn)生的系統(tǒng)最大可能執(zhí)行路徑不是系統(tǒng)反例.第二行和第四行的系統(tǒng)安全性概率非常低，根據(jù)觀測序列可知，系統(tǒng)的執(zhí)行機構(gòu)失效后,請求控制獲得授權(quán)，系統(tǒng)違背了安全屬性，即此時系統(tǒng)的最大可能執(zhí)行路徑是系統(tǒng)反例.通過對表2的分析可知，系統(tǒng)安全性預測結(jié)果和以最大可能執(zhí)行路徑作為反例的預測都可能產(chǎn)生錯誤，5.3節(jié)通過實驗評估本文方法的安全性和反例預測結(jié)果的錯誤率.算法預測精度和性能分析首先定義安全性預測的兩類錯誤(1)誤報，即系統(tǒng)是安全的,監(jiān)控器判定系統(tǒng)不安全，漏報，即系統(tǒng)進入了不安全狀態(tài)，監(jiān)控器判定系統(tǒng)是安全的.引起上述兩類錯誤不僅和本文方法預測精度有關(guān)也和系統(tǒng)安全性概率閾值的選擇相關(guān).例如，在給定閾值下，如果系統(tǒng)是安全的，但系統(tǒng)安全性概率低于閾值，引起監(jiān)控器誤報.相反，如果系統(tǒng)是不安全的，但系統(tǒng)安全性概率高于閾值，會引起監(jiān)控器漏報.反例預測錯誤是指系統(tǒng)違背安全屬性時，產(chǎn)生的最大可能執(zhí)行路徑不是反例.在此定義下，反例預測的錯誤和閾值無關(guān)，能真實反映本文方法反例預測的錯誤率.根據(jù)5.1節(jié)的模型和系統(tǒng)參數(shù)設(shè)置，不考慮安全性概率閾值，模擬運行系統(tǒng)400次，每次運行到系統(tǒng)違背安全屬性或觀測序列的長度大于50為止.在400次運行中系統(tǒng)違背安全屬性64次.通過分析系統(tǒng)每次運行的觀測序列、最大可能執(zhí)行路徑和系統(tǒng)實際執(zhí)行路徑，表3給出IIV算法和PF算法安全性預測錯誤率和本文提出的反例預測算法的錯誤率?當系統(tǒng)違背安全屬性時，我們的方法能夠給出反例而PF算法不能給出系統(tǒng)反例，在安全攸關(guān)系統(tǒng)中，漏報的危害比誤報要大，而IIV算法漏報次數(shù)只有PF算法的一半，預測錯誤率下降了近20%.表3IIV和PF算法預測錯誤率方法安全性預測反例預測誤報次數(shù)漏報次數(shù)預測錯誤率違背安全屬性次數(shù)反例預測錯誤數(shù)預測錯誤率IIV1830.0525PF2060.06506470.1094/安全性概率閾值的選擇也影響安全性預測的錯誤率.從圖4可以看出,隨著閾值增大，誤報率上升，漏報率下降.相反，隨著閾值減小，誤報率下降,漏報率上升.當閾值在0.8到0.9之間時，系統(tǒng)預測錯誤率達到最低，因此合理選擇安全性概率閾值能降低系統(tǒng)預測錯誤率，一般來說系統(tǒng)的漏報比誤報危害要大，適當提高閾值可以減少漏報率，就本例來說安全性概率閾值設(shè)置為0.9較為合理.下面比較兩種算法的時間和空間復雜性.在保證兩種方法具有相同計算精度的情況下，通過不斷增大系統(tǒng)模型狀態(tài)的數(shù)量，統(tǒng)計算法的執(zhí)行時間和消耗的內(nèi)存空間.圖5給出了兩種安全性驗證算法時間和空間隨系統(tǒng)狀態(tài)數(shù)增大的變化趨勢.從圖5可以看出，在時間性能方面，隨系統(tǒng)狀態(tài)數(shù)增大，IIV算法的執(zhí)行時間變化比較平穩(wěn)，PF算法執(zhí)行時間變化較快?在空間性能方面，IIV算法消耗的內(nèi)存空間隨系統(tǒng)狀態(tài)數(shù)增大變化不明顯，而PF算法在狀態(tài)數(shù)達到80以上時內(nèi)存空間增長較快?出現(xiàn)這種實驗結(jié)果的主要原因是：⑴IIV算法約簡了系統(tǒng)模型和屬性自動機的組合狀態(tài)減少了系統(tǒng)執(zhí)行時間和消耗的空間，而PF算法是直接基于系統(tǒng)模型和屬性自動機的組合狀態(tài)進行聯(lián)合概率分布的計算，(2)IIV算法每次僅處理一個觀測，而PF算法需要保存當前觀測之前的序列，(3)隨著系統(tǒng)狀態(tài)數(shù)增長，PF算法要保持和IIV算法相同的精度，必須增加粒子的數(shù)量從而引起計算時間和空間的增長變快.總結(jié)本文針對狀態(tài)不可觀測的且行為具有隨機性特征的CPS，提出了運行時安全性驗證方法，首先，構(gòu)造了運行時驗證框架，通過HMM來建模系統(tǒng)，使用DFA規(guī)約系統(tǒng)安全屬性的否定，兩者的乘積自動機作為運行時監(jiān)控器，將CPS運行時安全性驗證問題約簡到屬性監(jiān)控器上的概率推斷問題.然后，提出了一種增量迭代安全性驗證算法以及反例生成算法.實例分析和實驗結(jié)果表明本文提出的方法能正確地和快速地探測系統(tǒng)違背安全屬性的行為，并能夠產(chǎn)生有效的反例.本文沒有考慮CPS的混成系統(tǒng)特征，下一步工作是擴展HMM使其能夠建模隨機混成系統(tǒng)并對該類CPS進行運行時安全性驗證.參考文獻【相關(guān)文獻】黃志球，徐丙鳳,闞雙龍，胡軍，陳哲?嵌入式機載軟件安全性分析標準、方法及工具研究綜述J].軟件學報,2014,25(2):200-218.HuangZQ,XuBF,KanSL,HuJ,ChenZ.Surveyonembeddedsoftwaresafetyanalysisstandards,methodsandtoolsforairbornesystem[J].JournalofSoftware,2014,25(2):200-218.(inChinese)ChenF,YeH,YangJ,etal.Astandardizeddesignmethodologyforcomplexdigitallogiccomponentsofcyber-physicalsystems[J].Microprocessors&Microsystems,2015,39(8):1245-1254.ZhengX,JulienC,ChenH,etal.Real-timesimulationsupportforruntimeverificationofcyber-physicalsystems[J].ACMTransactionsonEmbeddedComputingSystems,2017,16(4):106.JiangY,SongH,WangR,etal.Data-centeredruntimeverificationofwirelessmedicalcyber-physicalsystem[J].IEEETransactionsonIndustrialInformatics,2017,13(4):1900-1909.MedhatR,BonakdarpourB,KumarD,etal.Runtimemonitoringofcyber-physicalsystemsundertimingandmemoryconstraints[J].ACMTransactionsonEmbeddedComputingSystems,2015,14(4):79-108.YuK,ChenZ,DongW.Apredictiveruntimeverificationframeworkforcyber-physicalsystems[A].IEEEEighthInternationalConferenceonSoftwareSecurityandReliability-Companion[C].SanFrancisco,California,USA:IEEE,2014.223-227.BakS,HuangZ,AbadFAT,etal.Safetyandprogressfordistributedcyber-physicalsystemswithunreliablecommunication[J].ACMTransactionsonEmbeddedComputingSystems,2015,14(4):1-22.MaoJ,ChenL.Runtimemonitoringforcyber-physicalsystems:acasestudyofcooperativeadaptivecruisecontrol[A].SecondInternationalConferenceonIntelligentSystemDesignandEngineeringApplication[C].Sanya,Hainan,China:IEEE,2012.509-515.SistlaAP,ZefranM,FengY,etal.Timelymonitoringofpartiallyobservablestochasticsystems[A].InternationalCo