羅晨霞, 王 瑞, 關(guān) 永, 李曉娟, 施智平 , Xiaoyu SONG

1(輕型工業(yè)機(jī)器人與安全驗(yàn)證北京市重點(diǎn)實(shí)驗(yàn)室(首都師范大學(xué) 信息工程學(xué)院),北京 100048)

2(電子系統(tǒng)可靠性與數(shù)理交叉學(xué)科國(guó)家國(guó)際科技合作示范型基地(首都師范大學(xué)),北京 100048)

3(Portland State University, Portland 97207, OR 97207, USA)

CPS是一個(gè)在環(huán)境感知的基礎(chǔ)上整合了物理和計(jì)算元素的系統(tǒng),可以智能地響應(yīng)真實(shí)世界場(chǎng)景的動(dòng)態(tài)變化.它通過(guò)計(jì)算進(jìn)程和物理進(jìn)程相互影響的反饋循環(huán)實(shí)現(xiàn)深度融合和實(shí)時(shí)交互增加或擴(kuò)展新的功能,以安全、可靠、高效和實(shí)時(shí)的方式監(jiān)測(cè)或是控制一個(gè)物理實(shí)體[1].從2006年2月《美國(guó)競(jìng)爭(zhēng)力計(jì)劃》將CPS列為重要的研究項(xiàng)目后,信息物理系統(tǒng)取得了很好的研究和發(fā)展[2].直至現(xiàn)在,CPS已經(jīng)涵蓋了小到智能家庭網(wǎng)絡(luò),大到工業(yè)控制系統(tǒng)和智能交通系統(tǒng),滲透到了航空、汽車(chē)、能源、醫(yī)療衛(wèi)生和物流等多個(gè)領(lǐng)域.隨著CPS的廣泛應(yīng)用,它的安全性問(wèn)題也越來(lái)越得到關(guān)注.其中,由于CPS在真實(shí)的物理環(huán)境中工作,各種環(huán)境因素對(duì)于CPS的影響是實(shí)際存在且不容忽視的,它們可能會(huì)導(dǎo)致CPS從傳感器中獲得的數(shù)據(jù)與實(shí)際環(huán)境不符,從而使得CPS做出錯(cuò)誤的或是危險(xiǎn)的行為[3-5].因此,在對(duì)CPS的安全性和可靠性研究中考慮物理環(huán)境的影響是非常有必要的.

保證系統(tǒng)安全性和可靠性的傳統(tǒng)手段有靜態(tài)分析、測(cè)試和模型檢測(cè)等.靜態(tài)分析是一種離線分析程序的技術(shù),旨在根據(jù)程序結(jié)構(gòu)來(lái)確定程序的屬性.通常這樣的靜態(tài)分析只能檢測(cè)一組有限的通用錯(cuò)誤,如數(shù)組綁定操作潛在的死鎖問(wèn)題,而且常常會(huì)產(chǎn)生誤報(bào)[6].測(cè)試是對(duì)選定的輸入數(shù)據(jù)集運(yùn)行系統(tǒng),通過(guò)比較所產(chǎn)出的輸出與預(yù)期值來(lái)判斷系統(tǒng)是否會(huì)有錯(cuò)誤,但依然存在測(cè)試用例不完備的問(wèn)題,通常不能保證系統(tǒng)絕對(duì)沒(méi)有錯(cuò)誤[7].與測(cè)試不同,模型檢測(cè)是針對(duì)某類(lèi)性質(zhì)來(lái)檢查系統(tǒng)是否合乎規(guī)約,它的基本思想是將一個(gè)過(guò)程或系統(tǒng)抽象成一個(gè)有窮狀態(tài)模型,然后加以分析驗(yàn)證.由于對(duì)系統(tǒng)空間的窮舉搜索,在并發(fā)系統(tǒng)中,其狀態(tài)的數(shù)據(jù)往往隨著并發(fā)分量的增加呈指數(shù)增長(zhǎng),因此,模型檢測(cè)會(huì)存在空間爆炸問(wèn)題.與以上這些傳統(tǒng)質(zhì)量保障技術(shù)相比,運(yùn)行時(shí)驗(yàn)證方法是一種輕量級(jí)的形式化方法,并且具有高度的可擴(kuò)展性[8-13],它對(duì)運(yùn)行的軟件系統(tǒng)進(jìn)行實(shí)時(shí)監(jiān)控,可以實(shí)時(shí)地驗(yàn)證系統(tǒng)的執(zhí)行路徑是否滿足屬性規(guī)范.由于運(yùn)行時(shí)驗(yàn)證方法是針對(duì)程序或者程序產(chǎn)生的蹤跡進(jìn)行分析的,并且系統(tǒng)在運(yùn)行時(shí)的執(zhí)行路徑是有窮的,因此不存在空間爆炸問(wèn)題.形式化驗(yàn)證方法作為傳統(tǒng)質(zhì)量保障方法的補(bǔ)充,已被應(yīng)用到了多個(gè)領(lǐng)域,如:無(wú)線傳感器應(yīng)用[14]、車(chē)輛總線系統(tǒng)[15]、C程序[16]和醫(yī)療系統(tǒng)[17]等.同樣地,在 CPS領(lǐng)域也取得了一定的成果.例如,針對(duì)CPS中計(jì)算和物理系統(tǒng)由于復(fù)雜交互出現(xiàn)的問(wèn)題,利用形式化驗(yàn)證方法檢測(cè)和驗(yàn)證了可能導(dǎo)致復(fù)雜交互失敗的條件.提出了改進(jìn)的形式化方法來(lái)驗(yàn)證CPS中組件的復(fù)雜性問(wèn)題,提高了CPS的可靠性[18].也有學(xué)者研究自動(dòng)轉(zhuǎn)換方法和規(guī)范邏輯語(yǔ)義以降低驗(yàn)證復(fù)雜性和運(yùn)行開(kāi)銷(xiāo)[19].對(duì)于特殊情況,如關(guān)于 CPS是分布式系統(tǒng)并且在動(dòng)態(tài)物理環(huán)境下存在離散控制問(wèn)題,有關(guān)學(xué)者提出了針對(duì)性的形式化驗(yàn)證方法和框架[20].

關(guān)于考慮物理環(huán)境對(duì) CPS的影響,國(guó)內(nèi)外已有相關(guān)研究.為了使自主機(jī)器人在遠(yuǎn)程感知的開(kāi)發(fā)研究中應(yīng)對(duì)環(huán)境的變化并允許探索全新的領(lǐng)域,Tabak等人介紹了一種算法,通過(guò)在環(huán)境中不同位置收集數(shù)據(jù)來(lái)生成或更新環(huán)境的3-D體積模型[21].為了解決CPS中由于多維異構(gòu)性導(dǎo)致的環(huán)境信息描述不統(tǒng)一的問(wèn)題和環(huán)境信息融合交互困難的問(wèn)題,于洋等人基于元建模設(shè)施和建模技術(shù),提出一種面向CPS環(huán)境信息的建模方法.該方法利用層次化的建模思想和領(lǐng)域化的建模方法,定義了環(huán)境信息的元元模型及不同領(lǐng)域中環(huán)境信息的元模型,實(shí)現(xiàn)了環(huán)境信息的元信息統(tǒng)一和不同領(lǐng)域中展現(xiàn)形式的多樣性[22].在醫(yī)療領(lǐng)域,允許工程師明確而精確地指定有關(guān)CPS設(shè)計(jì)的物理環(huán)境假設(shè),并通過(guò)算法將物理模型與系統(tǒng)模型相結(jié)合,利用 UPPAL進(jìn)行醫(yī)療器械的形式化驗(yàn)證[23].

本文針對(duì)物理環(huán)境的影響提出一種面向?qū)崟r(shí)數(shù)據(jù)的一體化建模方法,通過(guò)定義一系列規(guī)則,將環(huán)境模型集成到運(yùn)行時(shí)監(jiān)視模型中.該方法的原理是通過(guò)動(dòng)態(tài)調(diào)整監(jiān)視模型中的參數(shù)范圍,使得 CPS中的安全屬性在復(fù)雜的物理環(huán)境中仍然得到滿足.具體步驟是,首先建立環(huán)境的數(shù)學(xué)模型.然后,依據(jù)合并規(guī)則將數(shù)學(xué)模型進(jìn)行整合,整合的最終結(jié)果是,相同的系統(tǒng)參數(shù)有且僅有一個(gè)相同的環(huán)境模型.接著,定義了轉(zhuǎn)換規(guī)則,用偽代碼作為中間轉(zhuǎn)換語(yǔ)言描述環(huán)境模型.最后,根據(jù)組合規(guī)則將環(huán)境模型代碼組合到運(yùn)行時(shí)監(jiān)視模型中進(jìn)行驗(yàn)證.最后,本文搭建了 EV3實(shí)驗(yàn)平臺(tái),以移動(dòng)機(jī)器人避障為例,對(duì)電量續(xù)航進(jìn)行安全性提示,通過(guò)分析和建立環(huán)境模型,然后將此模型組合到監(jiān)視模型中,以使監(jiān)視模型更加完整,在不同物理環(huán)境中對(duì)續(xù)航時(shí)間的提示更加準(zhǔn)確.

本文第1節(jié)介紹運(yùn)行時(shí)驗(yàn)證方法的執(zhí)行過(guò)程和JavaMOP基礎(chǔ)知識(shí),為本文提到的運(yùn)行時(shí)監(jiān)視模型和環(huán)境建模方法的研究提供理論基礎(chǔ).第2節(jié)詳細(xì)介紹環(huán)境建模方法,定義了合并、轉(zhuǎn)換和組合規(guī)則,并舉例說(shuō)明.第3節(jié)對(duì)第 2節(jié)中提出的方法進(jìn)行實(shí)驗(yàn)評(píng)估,將影響電池容量的環(huán)境模型整合到監(jiān)視模型中進(jìn)行實(shí)驗(yàn)評(píng)估.第 4節(jié)總結(jié)本文工作.

1 預(yù)備知識(shí)

本節(jié)首先介紹了運(yùn)行時(shí)驗(yàn)證方法、原理和本文用到的運(yùn)行時(shí)驗(yàn)證工具框架,為本文后續(xù)的環(huán)境建模方法提供理論基礎(chǔ).

1.1 運(yùn)行時(shí)驗(yàn)證

運(yùn)行時(shí)驗(yàn)證是一種在線的、實(shí)時(shí)的形式化驗(yàn)證方法,它允許測(cè)試者使用數(shù)學(xué)的形式來(lái)指定系統(tǒng)并監(jiān)測(cè)這些屬性規(guī)約在系統(tǒng)運(yùn)行時(shí)是否是一直滿足的,當(dāng)系統(tǒng)行為違反屬性規(guī)約時(shí),激發(fā)處理程序給出提醒或是執(zhí)行用戶自定義程序引導(dǎo)系統(tǒng)到正確的行為.它避免了模型檢測(cè)方法的空間爆炸問(wèn)題和傳統(tǒng)測(cè)試的測(cè)試用例不完備問(wèn)題,是一種實(shí)時(shí)的、全自動(dòng)的、技術(shù)規(guī)模更小的質(zhì)量保障方法.

運(yùn)行時(shí)驗(yàn)證方法的原理是構(gòu)造實(shí)時(shí)時(shí)序邏輯的時(shí)間自動(dòng)機(jī).如果系統(tǒng)的執(zhí)行路徑表示為v=?1?2…?i…,其中,?i是一個(gè)時(shí)間狀態(tài),那么,運(yùn)行時(shí)驗(yàn)證方法則是將時(shí)間自動(dòng)機(jī)擴(kuò)展為監(jiān)視器來(lái)驗(yàn)證該執(zhí)行路徑是否滿足屬性規(guī)約.如圖 1所示,對(duì)一個(gè)系統(tǒng)進(jìn)行運(yùn)行時(shí)驗(yàn)證,首先,根據(jù)該系統(tǒng)的屬性規(guī)約生成監(jiān)視器.然后,將目標(biāo)系統(tǒng)置于監(jiān)控下,監(jiān)控器下的事件記錄器負(fù)責(zé)竊聽(tīng)目標(biāo)程序的數(shù)據(jù)和執(zhí)行狀態(tài),將目標(biāo)程序的每一次類(lèi)的加載、調(diào)用和函數(shù)的調(diào)用、執(zhí)行等操作進(jìn)行非侵入式的收集,這些操作將會(huì)隨著系統(tǒng)的執(zhí)行實(shí)時(shí)地、不斷地在存儲(chǔ)器中更新.狀態(tài)檢查器根據(jù)需要驗(yàn)證的屬性規(guī)范匹配系統(tǒng)狀態(tài),確定是否違背或滿足屬性.最后,通過(guò)執(zhí)行監(jiān)控程序給出驗(yàn)證結(jié)果,當(dāng)違背屬性時(shí),它會(huì)觸發(fā)處理程序,向目標(biāo)程序發(fā)送自定義的反饋信息,以便目標(biāo)程序可以意識(shí)到不安全的操作及時(shí)修正或是向用戶發(fā)出警示提醒.

運(yùn)行時(shí)驗(yàn)證根據(jù)監(jiān)控器監(jiān)控對(duì)象的不同有兩種應(yīng)用.一種是實(shí)時(shí)監(jiān)測(cè)正在執(zhí)行的行為序列,驗(yàn)證當(dāng)前行為是否滿足屬性規(guī)約,違背時(shí)給出提示,這種運(yùn)行時(shí)驗(yàn)證稱(chēng)為在線驗(yàn)證.另一種則監(jiān)測(cè)歷史執(zhí)行序列,離線分析存儲(chǔ)執(zhí)行路徑,被應(yīng)用在離線的自動(dòng)評(píng)估測(cè)試中,它被稱(chēng)為離線驗(yàn)證[24].對(duì)于 CPS系統(tǒng)來(lái)說(shuō),要求盡早地監(jiān)測(cè)違背安全屬性的行為,從而可以積極地做出反應(yīng),所以本文考慮的是在線驗(yàn)證方式.

1.2 JavaMOP語(yǔ)義

面向監(jiān)控的編程(monitor-oriented programming,簡(jiǎn)稱(chēng)MOP)是一個(gè)軟件開(kāi)發(fā)工具支持和分析框架,它支持面向方面編程的編織模式,支持多種形式化邏輯語(yǔ)言來(lái)描述屬性規(guī)約,是一個(gè)自動(dòng)化程序較高的運(yùn)行時(shí)驗(yàn)證框架[11].MOP工具會(huì)自動(dòng)地根據(jù)屬性規(guī)約合成監(jiān)視器,并將它們集成在應(yīng)用程序中.

MOP框架具有以下特點(diǎn).

(1) 將形式化規(guī)約和監(jiān)視代碼集成為一個(gè)系統(tǒng),允許開(kāi)發(fā)測(cè)試人員使用數(shù)學(xué)形式來(lái)指定系統(tǒng),并證明這些屬性.

(2) 它是一種輕量級(jí)的形式化方法,僅考慮一個(gè)模型的計(jì)算,而不是整個(gè)狀態(tài)空間模型的檢查.

(3) 具有邏輯語(yǔ)言的可擴(kuò)展性(可以在程序中的任何地方添加邏輯語(yǔ)句,可以指定過(guò)去或未來(lái)的狀態(tài)).其中,時(shí)序邏輯語(yǔ)言不僅限于純布爾命題的序列,還可以是具有時(shí)間特性的序列,即可以約束隨時(shí)間變化而變化的數(shù)據(jù)值的命題序列.

MOP框架可以實(shí)時(shí)地監(jiān)測(cè)系統(tǒng)的執(zhí)行,當(dāng)發(fā)現(xiàn)系統(tǒng)行為違背或滿足屬性規(guī)約時(shí)控制程序的執(zhí)行.這種控制使得用戶可以為當(dāng)前危險(xiǎn)行為提供處理程序,這些處理程序不僅可以向用戶報(bào)告錯(cuò)誤或拋出異常,還可以執(zhí)行更加復(fù)雜的動(dòng)作,例如重置狀態(tài)或重啟系統(tǒng).一個(gè)規(guī)范定義的運(yùn)行時(shí)監(jiān)視器可以自動(dòng)地組合到目標(biāo)系統(tǒng)中,以便在違背規(guī)約時(shí)及時(shí)地更正系統(tǒng)行為,保證系統(tǒng)的安全性和可靠性.MOP的實(shí)例包括 JavaMOP和 BusMOP,由于Java語(yǔ)言具有跨平臺(tái)性以及實(shí)驗(yàn)平臺(tái)EV3的第三方插件Lejos支持Java語(yǔ)言,所以本文應(yīng)用JavaMOP實(shí)例.完整語(yǔ)義如圖2所示[11].

JavaMOP支持的邏輯語(yǔ)言包括上下文無(wú)關(guān)語(yǔ)法(context free grammar,簡(jiǎn)稱(chēng) CFG)、線性時(shí)序邏輯(linear temporal logic,簡(jiǎn)稱(chēng)LTL)、有限自動(dòng)機(jī)(finite state machine,簡(jiǎn)稱(chēng)FSM)、過(guò)去時(shí)間的線性時(shí)序邏輯(past time linear temporal logic,簡(jiǎn)稱(chēng)ptLTL)等.它提供圖形用戶界面(graphical user interface,簡(jiǎn)稱(chēng)GUI)和命令行界面,用于編輯和處理規(guī)約.同時(shí)通過(guò)JavaMOP,用戶可以定義自己的屬性描述語(yǔ)言,具有可插拔性和靈活性.

JavaMOP主要包括5個(gè)部分:頭部、變量聲明、事件聲明、屬性的形式化描述和處理程序.

頭部:頭部包括修飾符、規(guī)范ID和參數(shù)列表3個(gè)部分.修飾符定義了監(jiān)視模型中事件的訪問(wèn)方式和索引方式.規(guī)約ID是用戶自定義名,即監(jiān)控模型的名稱(chēng),不可重復(fù)定義.

變量聲明:變量聲明和參數(shù)列表中的變量不同.參數(shù)列表中的變量是JavaMOP規(guī)范中的變量,通常情況下是監(jiān)控模型中的系統(tǒng)變量.而變量聲明是本地監(jiān)視器變量,可以在事件和屬性處理程序中修改.監(jiān)視器變量的作用多種多樣的,可以記錄監(jiān)視的狀態(tài),寫(xiě)日志等.其聲明方式和使用方法遵循Java語(yǔ)法.

事件聲明:其作用是定義事件.事件是指在目標(biāo)程序執(zhí)行過(guò)程中立即發(fā)生的一個(gè)動(dòng)作,在監(jiān)控程序中對(duì)應(yīng)于被監(jiān)控變量的設(shè)置與更新,或是被監(jiān)控方法的調(diào)用與執(zhí)行.JavaMOP的事件聲明遵循AspectJ語(yǔ)義[25],包含處理邏輯"advice"定義〈AspectJ advice〉和事件操作〈Java Statements〉,其中,事件操作部分可以通過(guò)Java編程修改被控程序或是監(jiān)視器狀態(tài).事件編織到 Java程序中后,將會(huì)記錄事件執(zhí)行的路徑,用來(lái)檢查是否符合屬性規(guī)約.另外,事件的聲明順序是有意義的,如果多個(gè)事件同時(shí)發(fā)生,最終監(jiān)視模型將按照事件的聲明順序執(zhí)行.

屬性定義:屬性在JavaMOP中是可選的,即一個(gè)MOP規(guī)范中可能包含多條屬性或沒(méi)有屬性.一條屬性由一個(gè)屬性描述邏輯名(〈LOGIC Name〉)和邏輯語(yǔ)義(〈LOGIC Syntax〉)構(gòu)成,之間以冒號(hào)隔開(kāi).由于運(yùn)行時(shí)驗(yàn)證方法監(jiān)視的是系統(tǒng)的執(zhí)行路徑,因此,屬性是一系列事件與邏輯的組合.MOP中規(guī)定屬性中所涉及到的所有事件必須是已定義的.JavaMOP支持的屬性描述語(yǔ)言包括FSM、ERE、CFG、ptLTL、LTL等.

處理器:處理器以@fail、@violation或@validation開(kāi)頭,分別代表自動(dòng)機(jī)的不確定、違背或滿足這3種狀態(tài).在〈Java Statements〉中用戶可以自定義動(dòng)作,在滿足處理器觸發(fā)條件時(shí)執(zhí)行.

2 環(huán)境建模方法

為了解決 CPS中由于環(huán)境影響導(dǎo)致的系統(tǒng)數(shù)據(jù)與實(shí)際環(huán)境不匹配的問(wèn)題,本文結(jié)合運(yùn)行時(shí)驗(yàn)證技術(shù),提出了一種在 CPS中應(yīng)對(duì)環(huán)境變化的一體化建模方法.該方法定義了合并規(guī)則、轉(zhuǎn)換規(guī)則和組合規(guī)則,將領(lǐng)域模型定義為數(shù)學(xué)模型,然后集成到監(jiān)控模型中.最終實(shí)現(xiàn)將環(huán)境信息分享到監(jiān)控模型中的目標(biāo),使得監(jiān)控程序的執(zhí)行更加精確,安全屬性在不確定的環(huán)境中始終得以滿足.

2.1 系統(tǒng)框架

一體化建模方法不改變運(yùn)行時(shí)驗(yàn)證方法的原理和執(zhí)行過(guò)程,該方法主要是在圖 1所示運(yùn)行時(shí)驗(yàn)證過(guò)程的基礎(chǔ)上,增加環(huán)境建模方法,對(duì)監(jiān)視模型中的屬性和參數(shù)產(chǎn)生影響,即對(duì)監(jiān)視模型生成的前期數(shù)據(jù)產(chǎn)生影響.系統(tǒng)框架如圖3所示.

在CPS中,屬性是由用戶提出的需求或是需求文檔中的內(nèi)容形式化后的規(guī)約,包括CPS的功能性需求、非功能性需求和設(shè)計(jì)約束這3個(gè)主要部分.目標(biāo)程序一般是指CPS控制器中的計(jì)算或控制程序,將監(jiān)視器插裝在控制器中,通過(guò)實(shí)時(shí)地監(jiān)測(cè)控制程序來(lái)驗(yàn)證CPS的執(zhí)行路徑是否滿足或違背安全屬性規(guī)約.對(duì)CPS進(jìn)行一體化建模,將環(huán)境影響集成到監(jiān)控模型中的過(guò)程如圖3所示.首先,由于數(shù)學(xué)具有抽象、精準(zhǔn)的特點(diǎn),將領(lǐng)域模型描述為數(shù)學(xué)模型.然后,根據(jù)合并規(guī)則標(biāo)準(zhǔn)化環(huán)境模型,主要是對(duì)作用于相同系統(tǒng)參數(shù)的不同環(huán)境模型進(jìn)行整合,即將影響同一個(gè)系統(tǒng)參數(shù)的所有環(huán)境影響關(guān)系都集合在一起進(jìn)行數(shù)學(xué)的劃分,使最終的環(huán)境模型之間不產(chǎn)生交集,這樣做可以避免發(fā)生驗(yàn)證邏輯錯(cuò)誤.因?yàn)檫\(yùn)行時(shí)驗(yàn)證工具眾多,使用的語(yǔ)言多種多樣,所以必須要有一個(gè)統(tǒng)一的表達(dá)方式,使得不同語(yǔ)言的使用者可以清晰的閱讀“中間模型”.而偽代碼結(jié)構(gòu)清晰、代碼簡(jiǎn)單、可讀性好,可以使得使用者很容易地以任何一種編程語(yǔ)言(Pascal、C、Java等)無(wú)歧義地實(shí)現(xiàn)算法,所以最后,定義轉(zhuǎn)換規(guī)則,將標(biāo)準(zhǔn)化模型轉(zhuǎn)換為偽代碼.最后,通過(guò)監(jiān)視模型對(duì)應(yīng)的編程語(yǔ)言,將環(huán)境模型的偽代碼遵循模型組合規(guī)則集成到運(yùn)行時(shí)監(jiān)視模型中.

在一個(gè)監(jiān)視模型中,事件在監(jiān)視程序執(zhí)行過(guò)程中通過(guò)捕獲被監(jiān)控的操作來(lái)獲取參數(shù),其中,部分參數(shù)會(huì)參與到事件操作的計(jì)算中,這類(lèi)參數(shù)被稱(chēng)為系統(tǒng)參數(shù).系統(tǒng)參數(shù)的值可能會(huì)受到環(huán)境的影響而發(fā)生變化,在監(jiān)視模型不知曉這種變化關(guān)系而執(zhí)行運(yùn)行時(shí)監(jiān)視時(shí),會(huì)出現(xiàn)無(wú)法正確識(shí)別 CPS不符合實(shí)際環(huán)境的危險(xiǎn)行為,從而不會(huì)發(fā)出安全提醒的情況.該建模方法在標(biāo)準(zhǔn)化環(huán)境模型后,將轉(zhuǎn)化的偽代碼通過(guò)特定的語(yǔ)言寫(xiě)入事件操作中,將環(huán)境影響映射到系統(tǒng)參數(shù)的值域選擇,從而使得參數(shù)可以隨著環(huán)境的變化而發(fā)生改變,達(dá)到環(huán)境自適應(yīng)的目的.這一過(guò)程不影響運(yùn)行時(shí)驗(yàn)證過(guò)程,只對(duì)監(jiān)視模型中事件的操作部分進(jìn)行執(zhí)行前的修改.

2.2 環(huán)境建模的規(guī)則描述

2.2.1 物理環(huán)境的數(shù)學(xué)模型定義

物理環(huán)境對(duì) CPS行為產(chǎn)生影響的原因是系統(tǒng)中的某些參數(shù)會(huì)因?yàn)槲锢硪蛩氐母淖兌l(fā)生變化,具體體現(xiàn)為系統(tǒng)的動(dòng)態(tài)輸入發(fā)生偏差,從而影響控制系統(tǒng)的邏輯判斷,故而波及到 CPS的行為.要避免這種影響,首先需要確定系統(tǒng)參數(shù)和物理環(huán)境的關(guān)系.這里先定義相關(guān)的符號(hào)表示,系統(tǒng)參數(shù)的集合S={s1,…,si,…,sn},環(huán)境參數(shù)的集合E={e1,…,ej,…,em},其中,集合中的每一個(gè)元素都用一個(gè)二元組(name,type)表示.下面是對(duì)物理環(huán)境的相關(guān)定義.

定義 1(環(huán)境數(shù)學(xué)模型).用一個(gè)三元組M(s,E′,R)來(lái)描述環(huán)境數(shù)學(xué)模型.其中,s∈S,是一個(gè)系統(tǒng)參數(shù).E′∈E,是一組會(huì)對(duì)s產(chǎn)生影響的環(huán)境因素的集合.R是s和E′之間的一組數(shù)學(xué)關(guān)系的集合{r1,...,rk,...,rl}.

定義 2(關(guān)系模型).關(guān)系模型r∈R由一個(gè)三元組(F,VC,L)定義.其中,F是函數(shù)的聲明部分,包括函數(shù)名、函數(shù)的參數(shù)和返回值類(lèi)型.F指明了系統(tǒng)參數(shù)s在整個(gè)系統(tǒng)代碼中出現(xiàn)的位置.VC是一個(gè)二元組(value(s),C(E′)),其中,C(E′)是物理?xiàng)l件,所以VC表示在條件C(E′)下的系統(tǒng)參數(shù)s的值為value(s).L是在此條件下該環(huán)境參數(shù)對(duì)系統(tǒng)參數(shù)的影響級(jí)別,影響級(jí)別是一系列的整數(shù),從1開(kāi)始,數(shù)值越大代表影響程度越小.此影響級(jí)別由領(lǐng)域模型定義.

例1:假設(shè)CPS的電池初始容量為1Ah,也就是說(shuō),電池每小時(shí)提供1A.溫度對(duì)電池容量存在影響[22].

S1:當(dāng)溫度t在[15°C,35°C]時(shí),電池容量不變.

S2:當(dāng)溫度t在[-10°C,15°C)時(shí),C=1-2×(25-T)÷100.

以上述兩種場(chǎng)景為例建立數(shù)學(xué)模型.這個(gè)例子涉及到了兩個(gè)物理變量,溫度T=(t,real)和Battery=(C,real).上述兩種場(chǎng)景列出了這兩個(gè)環(huán)境變量的兩種關(guān)系,假設(shè)建立的環(huán)境數(shù)學(xué)模型為M0,關(guān)系模型為R0,則此例所對(duì)應(yīng)的數(shù)學(xué)模型為M0(Battery,T,R0).為了便于撰寫(xiě),這里為復(fù)雜的式子定義了別名.

c1:15≤t≤35,

c2:-10≤t<15,

v2:C=1-2×(25-T)÷100.

假設(shè)溫度對(duì)電池的影響級(jí)別為1,系統(tǒng)變量C存在于函數(shù)handle中,根據(jù)S1和S2這兩種情況,關(guān)系模型R0建立為{r01,r02},具體如下.

r01:(handle,(1,c1),1),

r02:(handle,(v2,c2),1).

另外,電池電容還受到環(huán)境濕度H的影響[22],具體關(guān)系如下.

S3:當(dāng)環(huán)境濕度H在[10%RH,30%RH]時(shí),電池容量下降10%.例如,若原電池容量C=1,則當(dāng)電池處在該環(huán)境濕度后,C=0.9.

S4:當(dāng)溫度t在[40%RH,60%RH]時(shí),電池容量不變.

同理,定義別名:

c3:0.1≤h≤0.3,

c4:0.4≤h≤0.6.

假設(shè)該環(huán)境關(guān)系建立數(shù)學(xué)模型為M1,關(guān)系模型為R1,影響級(jí)別為 2,則此例所對(duì)應(yīng)的數(shù)學(xué)模型為M1(Battery,H,R1).關(guān)系模型R1為{r11,r12}.

r11:(handle,(0.9,c3),2),

r12:(handle,(1,c4),2).

在一個(gè)完整的數(shù)學(xué)模型中,VC應(yīng)具有完備性,也就是說(shuō),不論環(huán)境處于怎樣的狀態(tài),都能在VC集合中找到一個(gè)二元組(value(s),C(E′))與之匹配,同時(shí),C(E′)之間互斥不相交.這樣,在運(yùn)行時(shí)驗(yàn)證時(shí),在特定場(chǎng)景下的篩選結(jié)果是唯一的,因此程序執(zhí)行路徑是唯一確定的、無(wú)歧義的.

2.2.2 環(huán)境模型的合并規(guī)則

一個(gè)系統(tǒng)參數(shù)可能會(huì)受到多個(gè)物理因素的影響,同樣地,一個(gè)物理因素也可能會(huì)影響到多個(gè)系統(tǒng)參數(shù).它們之間的關(guān)系是復(fù)雜的,在領(lǐng)域知識(shí)中,這些數(shù)學(xué)關(guān)系表達(dá)是簡(jiǎn)單的,但在運(yùn)行時(shí)驗(yàn)證中也是很難操作的,因?yàn)闊o(wú)法有效地避免同一個(gè)系統(tǒng)參數(shù)的不同影響因素之間的關(guān)系是完備且互斥的.因此,需要通過(guò)制定規(guī)則來(lái)規(guī)范化和標(biāo)準(zhǔn)化這些獨(dú)立的數(shù)學(xué)模型,將多個(gè)相同系統(tǒng)參數(shù)單個(gè)物理影響因素的數(shù)學(xué)模型合并為一個(gè)系統(tǒng)參數(shù)多個(gè)物理影響因素的數(shù)學(xué)模型.此規(guī)則為后續(xù)將數(shù)學(xué)模型轉(zhuǎn)換為偽代碼提供邏輯基礎(chǔ).

假設(shè)有兩個(gè)環(huán)境模型M2(s2,E2′,R2)和M3(s3,E3′,R3),如果s2=s3,則這兩個(gè)對(duì)同一個(gè)系統(tǒng)參數(shù)建立的數(shù)學(xué)模型可以進(jìn)行合并,合并結(jié)果為M(s,E′,R),其中,s=s2(s3),具體的合并規(guī)則定義如下.

前提條件:系統(tǒng)參數(shù)相同是判斷兩個(gè)模型是否可以合并的前提條件.

模型計(jì)算規(guī)則:集合M{m1,m2,…,mm}和N{n1,n2,…,nn}做組合操作會(huì)得到f(m,n)個(gè)結(jié)果,其中,每?jī)蓚€(gè)元素取“&&”,得到的結(jié)果之間取“||”,即{m1&&n1||m1&&n2||…||mm&&nn}.

模型合并規(guī)則(1).模型合并規(guī)則(1)也叫作模型內(nèi)標(biāo)準(zhǔn)化規(guī)則,是一種針對(duì)關(guān)系模型的合并規(guī)則.具體為關(guān)系模型集合內(nèi)的元素之間作“||”操作.其中,VC執(zhí)行“||”操作,F和L不變.如M2中的關(guān)系模型R2={r21,r22,…,r2n},執(zhí)行此規(guī)則變?yōu)樾碌腞2={r21||r22||…||r2n}={F2,(VC21||VC22||…||VC2n),L2},M3同理.

模型合并規(guī)則(2).如果E2′=E3′,F2!=F3,即系統(tǒng)參數(shù)s在系統(tǒng)代碼中的函數(shù)位置不同,那么,環(huán)境模型則相互獨(dú)立,無(wú)需合并.為了規(guī)范化書(shū)寫(xiě),M可以寫(xiě)成(s,{E2′,E3′},R2∪R3),也可以保持不變.例如:在M2模型中,R2=(F2,VC2,L2),在M3模型中,R3=(F3,VC3,L3),F2!=F3,規(guī)范化書(shū)寫(xiě)后M的R={R2∪R3}={(F2,VC2,L2)∪(F3,VC3,L3)}.

模型合并規(guī)則(3).模型合并規(guī)則(3)也叫作模型間標(biāo)準(zhǔn)化規(guī)則.如果E2′!=E3′且F2=F3,即系統(tǒng)參數(shù)s的物理影響因素不同,但在系統(tǒng)代碼中的函數(shù)位置相同.合并規(guī)則為E={E2′,E3′},關(guān)系模型R中F=F2(F3),VC執(zhí)行模型計(jì)算規(guī)則,L取L2和L3中的最小值,即L=Min{L2,L3}.在組合條件下,系統(tǒng)參數(shù)的值value(s)取影響級(jí)別最大的值,即Worst{value2(s),value3(s)}.

這里不存在E2′=E3′且F2=F3的情況,因?yàn)樵谝粋€(gè)環(huán)境模型M(s,E′,R)中,對(duì)于一個(gè)系統(tǒng)參數(shù)s和特定的E′,R是具有完備性的.當(dāng)環(huán)境模型不符合合并規(guī)則的前提條件時(shí),執(zhí)行模型合并規(guī)則(1),對(duì)自身進(jìn)行規(guī)范化操作.模型合并規(guī)則(2)和規(guī)則(3)是模型之間的合并規(guī)則,其中,系統(tǒng)參數(shù)是否在同一個(gè)函數(shù)中是決定環(huán)境模型之間是否可以合并的關(guān)鍵.多于兩個(gè)模型進(jìn)行規(guī)范化合并時(shí),兩兩執(zhí)行合并規(guī)則,直到不滿足合并的前提條件.當(dāng)存在多種物理因素影響多個(gè)系統(tǒng)參數(shù)的情況時(shí),依據(jù)模型合并的前提條件,分別將具有相同系統(tǒng)參數(shù)的數(shù)學(xué)模型遵循規(guī)則合并.

例 2:假設(shè)M2(s2,E2′,R2)中的E2′和M3(s3,E3′,R3)中的E3′不相等且F2=F3,R2={r21,r22},R3={r31,r32},其中,VC2={VC21,VC22},VC3={VC31,VC32}.關(guān)系模型的每一個(gè)元素的展開(kāi)式如下.

R21:(F,VC21,L2)=(F,(value21(s),C21),L2).

R22:(F,VC22,L2)=(F,(value22(s),C22),L2).

R31:(F,VC31,L3)=(F,(value31(s),C31),L3).

R32:(F,VC32,L3)=(F,(value32(s),C32),L3).

現(xiàn)在對(duì)M2和M3兩個(gè)模型進(jìn)行合并,由本小節(jié)開(kāi)始時(shí)的假設(shè)可知s2=s3,因此符合前提條件,可以進(jìn)行合并.由E2′!=E3′且F2=F3,根據(jù)模型合并規(guī)則(3),合并后的模型M中E′={E2′,E3′},關(guān)系模型R中F=F2(F3),VC遵循組合規(guī)則“其中每?jī)蓚€(gè)元素取“&&”,得到的結(jié)果之間取“||””,最終的關(guān)系模型為R=((r21&&r31)||(r21&&r32)||(r22&&r31)||(r22&&r32)).以 (r21&&r31)為 例 ,(r21&&r31)=(F,(Worst{value21(s),value22(s)},C21(E2′)&&C31(E3′)),min{L2,L3}).

在例1中的模型M0(Battery,T,R0)和M1(Battery,H,R1)中,由于系統(tǒng)參數(shù)相同,都為Battery,滿足模型組合的前提條件,即M0和M1可以進(jìn)行組合.由于T!=H,即環(huán)境影響因素不同,分別是溫度和濕度,所以符合模型合并規(guī)則(3).對(duì)M0和M1執(zhí)行組合規(guī)則后形成的新模M為M=(Battery,{T,H},Worst{1,2})=(Battery,{T,H},1),R=(handle,(r01&&r11)||(r01&&r12)||(r02&&r11)||(r02&&r12),1),展開(kāi)式如圖4所示.

2.2.3 環(huán)境模型與偽代碼的轉(zhuǎn)換規(guī)則

對(duì)環(huán)境建立數(shù)學(xué)模型的最終目的是要將此模型組合到運(yùn)行時(shí)監(jiān)視模型中,使得在線監(jiān)視過(guò)程加入了環(huán)境變化的影響,讓安全屬性能夠在不確定的物理環(huán)境中一直滿足.在組合之前,為了相關(guān)領(lǐng)域人員和測(cè)試開(kāi)發(fā)人員都能夠簡(jiǎn)單、明了地表達(dá)和實(shí)現(xiàn)數(shù)學(xué)模型,本文提出將偽代碼作為中間轉(zhuǎn)化代碼.偽代碼是一種算法描述語(yǔ)言,其結(jié)構(gòu)清晰且可讀性好,并且類(lèi)似自然語(yǔ)言.用它來(lái)描述數(shù)學(xué)模型,可以使使用者以任何一種編程語(yǔ)言容易地、無(wú)歧義地實(shí)現(xiàn)算法.對(duì)于任意一個(gè)M(s,E′,R),關(guān)系模型為R(F,(value(s),C(E′)),L)的數(shù)學(xué)模型,轉(zhuǎn)換規(guī)則分為以下幾步.

(1) 根據(jù)關(guān)系模型中的F生成函數(shù).

(2) 變量聲明:在函數(shù)中,如果s不是函數(shù)的本地參數(shù),生成一個(gè)s變量并初始化.

(3) 根據(jù)(value(s),C(E′))生成條件判斷語(yǔ)句,其中,C(E′)為條件判斷,value(s)為在當(dāng)前條件下s的值.其中,特殊符號(hào)“||”在程序中代表“else if”.

(4) “U”符號(hào)出現(xiàn),則重新生成一個(gè)新的函數(shù),執(zhí)行(1)～(3)步.環(huán)境模型轉(zhuǎn)換為偽代碼的關(guān)鍵是(value(s),C(E′)對(duì)的邏輯轉(zhuǎn)換,將環(huán)境對(duì)系統(tǒng)參數(shù)的關(guān)系轉(zhuǎn)換為程序邏輯語(yǔ)言,便于之后集成到監(jiān)控模型中.第(2)步中的變量聲明是偽代碼中的語(yǔ)法需要,在監(jiān)視模型中,s由模型中的事件捕獲得到.

例3:在例2中,對(duì)模型M0(Battery,T,R0)和M1(Battery,H,R1)進(jìn)行了標(biāo)準(zhǔn)化,得到數(shù)學(xué)模型M(Battery,{T,H},1),其中,關(guān)系模型R=(handle,(r01&&r11)||(r01&&r12)||(r02&&r11)||(r02&&r12),1).接下來(lái),通過(guò)執(zhí)行以下步驟,將M轉(zhuǎn)換為偽代碼.

(1) 依據(jù)R中的F生成handle函數(shù).

(2) 聲明battery變量,并賦值為0.在使用編程語(yǔ)言實(shí)現(xiàn)時(shí),如果該變量已經(jīng)存在于函數(shù)的參數(shù)列表中,則步驟2可省略.

(3) 根據(jù)關(guān)系模型中的VC關(guān)系建立if邏輯部分.

最終M偽代碼如Pseudocode 1所示.將數(shù)學(xué)模型轉(zhuǎn)化為偽代碼后,測(cè)試開(kāi)發(fā)人員則負(fù)責(zé)將偽代碼實(shí)現(xiàn)為具體編程語(yǔ)言的程序并整合到運(yùn)行時(shí)監(jiān)視模型中,最后利用運(yùn)行時(shí)驗(yàn)證工具對(duì)模型中描述的屬性進(jìn)行安全性驗(yàn)證.在本文中,運(yùn)行時(shí)驗(yàn)證工具為JavaMOP,所以M模型的偽代碼用Java實(shí)現(xiàn)后組合到監(jiān)視模型中,如圖5中為M的Java實(shí)現(xiàn)代碼.

2.2.4 環(huán)境模型和運(yùn)行時(shí)監(jiān)視模型的組合規(guī)則

組合規(guī)則的目的是要將偽代碼實(shí)現(xiàn)為具體編程語(yǔ)言的程序后組合到監(jiān)視模型的事件操作部分,具體組合規(guī)則分為以下幾個(gè)步驟.

(1) 遍歷所有運(yùn)行時(shí)監(jiān)視模型的事件定義,選擇事件切入點(diǎn)的函數(shù)和模型代碼中的函數(shù)F相同的事件,且在事件操作中含有s參數(shù)參與計(jì)算.

(2) 選定代碼塊:其中,代碼塊的開(kāi)始是第1條s在賦值等號(hào)右邊的語(yǔ)句,代碼塊的結(jié)束時(shí)是最后一條s在賦值等號(hào)右邊的語(yǔ)句.

(3) 將代碼塊作為整體替換模型代碼中if條件控制的執(zhí)行語(yǔ)句.如果存在一個(gè)代碼塊對(duì)應(yīng)于多個(gè)模型代碼的情況,即多個(gè)模型代碼中的系統(tǒng)參數(shù)出現(xiàn)在同一個(gè)表達(dá)式中,此時(shí)將所有模型代碼中的 if條件組合操作后的新模型代碼替換掉原代碼塊.

(4) 賦值號(hào)右邊的s被置換為模型代碼中相同判斷條件執(zhí)行語(yǔ)句中的s的新值.

(5) 將最終形成的函數(shù)代碼插入到當(dāng)前事件中替換代碼塊.

連接點(diǎn)是切面插入應(yīng)用程序的地方,包含函數(shù)的調(diào)用和執(zhí)行、構(gòu)造函數(shù)的調(diào)用和執(zhí)行、變量的獲取與設(shè)置等.而切入點(diǎn)的作用則是過(guò)濾這些連接點(diǎn),匹配符合條件的連接點(diǎn)從而激活事件.它是連接點(diǎn)的子集合,在組合規(guī)則中,代碼塊的劃分是關(guān)鍵,將修改目標(biāo)鎖定在系統(tǒng)參數(shù)參與計(jì)算的語(yǔ)句上,以便于添加環(huán)境條件.

例4:例3中生成M的偽代碼后,使用Java語(yǔ)言編寫(xiě)函數(shù)實(shí)現(xiàn)偽代碼中的算法邏輯,按照組合規(guī)則將其插入到運(yùn)行時(shí)監(jiān)視模型中,步驟如下.

(1) 遍歷所有運(yùn)行時(shí)監(jiān)視模型的事件定義,并選擇函數(shù)與handle相同的事件.如圖6所示,在electricity驗(yàn)證模型的start、init和sufficientElectricity這3個(gè)事件中,只有init事件滿足要求,且系統(tǒng)參數(shù)battery參與了危險(xiǎn)距離b變量的賦值計(jì)算.

(2) 選定第1條battery在賦值等號(hào)右邊的語(yǔ)句作為代碼塊的開(kāi)始,最后一條battery在賦值等號(hào)右邊的語(yǔ)句作為代碼塊的結(jié)束,劃定代碼塊區(qū)域.如圖6中紅框所示,代碼塊包含b=battery×3.0÷w一條語(yǔ)句.

(3) 將代碼塊作為整體替換模型代碼中if條件控制的執(zhí)行語(yǔ)句,如圖7所示.

將賦值號(hào)右邊的battery置換為模型代碼中相同判斷條件執(zhí)行語(yǔ)句中的battery的新值,如圖8所示.最后,所獲得的結(jié)果如圖9所示.

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

本文的實(shí)驗(yàn)平臺(tái)選用了如圖 10所示的 EV3機(jī)器人,它是樂(lè)高公司開(kāi)發(fā)的第三代MINDSTORMS機(jī)器人,于2013年下半年上市.它不僅能夠加載多種傳感器,如超聲波傳感器、觸碰傳感器、陀螺儀等,而且還可以使用leJOS第三方庫(kù)支持Java語(yǔ)言編程.實(shí)驗(yàn)中,傳感器的采樣頻率設(shè)為1s,電池電壓為3.0v,容量為1Ah.

實(shí)驗(yàn)設(shè)計(jì)為移動(dòng)機(jī)器人勻速行駛執(zhí)行避障任務(wù)[26,27],每一次執(zhí)行時(shí)間至少需要 10min.機(jī)器人將使用超聲波傳感器和觸碰傳感器來(lái)感知周?chē)h(huán)境避開(kāi)障礙物.為了使移動(dòng)機(jī)器人成功地執(zhí)行避障任務(wù),設(shè)定一條安全屬性為“當(dāng)電池續(xù)航不足10分鐘時(shí)給出提示”.分析影響電池容量的環(huán)境因素,如例1～例4所示,將影響電池電容的溫度和濕度建立環(huán)境模型并組合到electricity監(jiān)視模型中去.已知存在關(guān)系式:容量(Ah)×電壓(V)=功率(W)×?xí)r間(h),在滿足電量條件下執(zhí)行了6 000多次實(shí)驗(yàn),實(shí)驗(yàn)結(jié)果見(jiàn)表1.

Table 1 Experimental results表1 實(shí)驗(yàn)結(jié)果

當(dāng)不考慮環(huán)境影響因素時(shí),理論上當(dāng)移動(dòng)機(jī)器人的功率為 18W 時(shí),會(huì)提示“在當(dāng)前功率下電池續(xù)航不足十分鐘!”.但當(dāng)環(huán)境中溫度和濕度發(fā)生變化時(shí)會(huì)出現(xiàn)續(xù)航時(shí)間比提示時(shí)間略長(zhǎng)或縮短的情況.由表 1可以看出,當(dāng)溫度在 15°C～35°C 時(shí),電池電容與濕度有關(guān).當(dāng)溫度在-10°C～15°C 時(shí),電池電容只與溫度有關(guān),與濕度無(wú)關(guān).將環(huán)境模型組合到運(yùn)行時(shí)監(jiān)視模型中,可以隨著環(huán)境中溫度和濕度的改變而調(diào)整電容值,從而調(diào)整安全提示的功率臨界值.

實(shí)驗(yàn)結(jié)果表明,監(jiān)視模型集成環(huán)境模型后,監(jiān)視程序的執(zhí)行將會(huì)更加精確,可以有效地保證在復(fù)雜工作環(huán)境下機(jī)器人系統(tǒng)的安全性和可靠性.該建模方法不僅可以用于移動(dòng)機(jī)器人的安全電量監(jiān)測(cè),也適用于采用運(yùn)行時(shí)驗(yàn)證方法保障系統(tǒng)的安全性和可靠性的CPS,不限制邏輯描述語(yǔ)言和操作系統(tǒng)類(lèi)型.

4 總 結(jié)

本文提出一種面向?qū)崟r(shí)數(shù)據(jù)的CPS一體化建模方法,對(duì)環(huán)境進(jìn)行建模,然后對(duì)環(huán)境模型進(jìn)行標(biāo)準(zhǔn)化,轉(zhuǎn)化為偽代碼后組合到監(jiān)視模型中進(jìn)行運(yùn)行時(shí)驗(yàn)證,目的是使得監(jiān)視模型更加完整、準(zhǔn)確,在環(huán)境發(fā)生變化時(shí),通過(guò)動(dòng)態(tài)調(diào)整模型中的參數(shù)范圍,使得 CPS中的安全屬性在復(fù)雜的物理環(huán)境中仍然得以滿足.該方法定義了模型合并規(guī)則、模型和偽代碼之間的轉(zhuǎn)換規(guī)則、環(huán)境模型和監(jiān)視模型的組合規(guī)則,并通過(guò)溫度和濕度對(duì)電池容量的影響舉例加以說(shuō)明.最后在移動(dòng)機(jī)器人平臺(tái)上,通過(guò)使用JavaMOP驗(yàn)證安全屬性的實(shí)驗(yàn)證明在機(jī)器人系統(tǒng)中組合物理模型后可以使得監(jiān)視模型的監(jiān)視更加準(zhǔn)確.