羅晨霞, 王 瑞, 關 永, 李曉娟, 施智平 , Xiaoyu SONG

1(輕型工業(yè)機器人與安全驗證北京市重點實驗室(首都師范大學 信息工程學院),北京 100048)

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

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

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

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

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

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

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

1 預備知識

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

1.1 運行時驗證

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

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

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

1.2 JavaMOP語義

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

MOP框架具有以下特點.

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

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

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

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

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

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

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

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

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

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

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

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

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

2.1 系統(tǒng)框架

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

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

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

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

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

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

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

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

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

S1:當溫度t在[15°C,35°C]時,電池容量不變.

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

以上述兩種場景為例建立數學模型.這個例子涉及到了兩個物理變量,溫度T=(t,real)和Battery=(C,real).上述兩種場景列出了這兩個環(huán)境變量的兩種關系,假設建立的環(huán)境數學模型為M0,關系模型為R0,則此例所對應的數學模型為M0(Battery,T,R0).為了便于撰寫,這里為復雜的式子定義了別名.

c1:15≤t≤35,

c2:-10≤t<15,

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

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

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

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

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

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

S4:當溫度t在[40%RH,60%RH]時,電池容量不變.

同理,定義別名:

c3:0.1≤h≤0.3,

c4:0.4≤h≤0.6.

假設該環(huán)境關系建立數學模型為M1,關系模型為R1,影響級別為 2,則此例所對應的數學模型為M1(Battery,H,R1).關系模型R1為{r11,r12}.

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

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

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

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

一個系統(tǒng)參數可能會受到多個物理因素的影響,同樣地,一個物理因素也可能會影響到多個系統(tǒng)參數.它們之間的關系是復雜的,在領域知識中,這些數學關系表達是簡單的,但在運行時驗證中也是很難操作的,因為無法有效地避免同一個系統(tǒng)參數的不同影響因素之間的關系是完備且互斥的.因此,需要通過制定規(guī)則來規(guī)范化和標準化這些獨立的數學模型,將多個相同系統(tǒng)參數單個物理影響因素的數學模型合并為一個系統(tǒng)參數多個物理影響因素的數學模型.此規(guī)則為后續(xù)將數學模型轉換為偽代碼提供邏輯基礎.

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

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

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

模型合并規(guī)則(1).模型合并規(guī)則(1)也叫作模型內標準化規(guī)則,是一種針對關系模型的合并規(guī)則.具體為關系模型集合內的元素之間作“||”操作.其中,VC執(zhí)行“||”操作,F和L不變.如M2中的關系模型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)參數s在系統(tǒng)代碼中的函數位置不同,那么,環(huán)境模型則相互獨立,無需合并.為了規(guī)范化書寫,M可以寫成(s,{E2′,E3′},R2∪R3),也可以保持不變.例如:在M2模型中,R2=(F2,VC2,L2),在M3模型中,R3=(F3,VC3,L3),F2!=F3,規(guī)范化書寫后M的R={R2∪R3}={(F2,VC2,L2)∪(F3,VC3,L3)}.

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

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

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

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).

現在對M2和M3兩個模型進行合并,由本小節(jié)開始時的假設可知s2=s3,因此符合前提條件,可以進行合并.由E2′!=E3′且F2=F3,根據模型合并規(guī)則(3),合并后的模型M中E′={E2′,E3′},關系模型R中F=F2(F3),VC遵循組合規(guī)則“其中每兩個元素取“&&”,得到的結果之間取“||””,最終的關系模型為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)參數相同,都為Battery,滿足模型組合的前提條件,即M0和M1可以進行組合.由于T!=H,即環(huán)境影響因素不同,分別是溫度和濕度,所以符合模型合并規(guī)則(3).對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),展開式如圖4所示.

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

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

(1) 根據關系模型中的F生成函數.

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

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

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

例3:在例2中,對模型M0(Battery,T,R0)和M1(Battery,H,R1)進行了標準化,得到數學模型M(Battery,{T,H},1),其中,關系模型R=(handle,(r01&&r11)||(r01&&r12)||(r02&&r11)||(r02&&r12),1).接下來,通過執(zhí)行以下步驟,將M轉換為偽代碼.

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

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

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

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

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

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

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

(2) 選定代碼塊:其中,代碼塊的開始是第1條s在賦值等號右邊的語句,代碼塊的結束時是最后一條s在賦值等號右邊的語句.

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

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

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

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

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

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

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

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

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

3 實驗評估

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

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

Table 1 Experimental results表1 實驗結果

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

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

4 總 結

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